Как связать нотацию с типом

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.

Основываясь на сертифицированном программировании Адама Чипалы с зависимыми типами , я бы ожидал, что какой-то вариант этого проанализирует 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.