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

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 的Certified Programming with Dependent Types，我本以为它的一些变体可以解析A |- B为entails A B任何时候A并且B已知为nat. 但这不会发生。知道为什么吗？

标签： coq

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.