如何将符号范围绑定到类型

Question

考虑以下玩具开发：

Declare Scope entails_scope.
Bind Scope entails_scope with nat.

Reserved Notation "A |- B" (at level 60, no associativity).
Inductive entails: nat -> nat -> Prop :=
| id {A}: A |- A

where "A |- B" := (entails A B) : entails_scope.

(* Fails with message: 'Unknown interpretation for notation "_ |- _".' *)
Fail Goal exists (A B: nat), A |- B.

基于Adam Chlipala的具有相关类型的认证程序，我希望只要知道A |- B和entails A B为A，都可以将其某些变体解析为B为nat。但这不会发生。知道为什么吗？

Answer 1

您可能要打开新引入的作用域

Open Scope entails_scope.
Goal exists (A B: nat), A |- B.

或明确指定

Delimit Scope entails_scope with E.
Goal exists (A B: nat), (A |- B)%E.