如何将注释作用域绑定到类型

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已知为nat，就会有某种变体将A |- B解析为entails A B。但这并没有发生。知道为什么吗？

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.