coq - 防止在 Coq 中应用后意外展开

Question

我的符号在申请后无意中展开了。每次我使用前装式时，我都不想在小示例文本的最后一行调用策略“更改”。如何禁止 Coq 展开我的 Notation "(a '==' b )"？

Require Export Coq.Vectors.Vector.
Import VectorNotations.
Inductive Terms : Type :=
    FVC : nat -> Terms.
Definition Fo:=nat.
Context (axs0 : nat -> Type).
Context (Atom : Vector.t Terms 2 -> Fo).
Notation "( a '==' b )" := (Atom [a:Terms; b:Terms]).
Notation "( A --> B )" := (A + B).

Inductive GPR (axs : nat -> Type) (ctx:list nat) : nat -> Type :=
| MP (A B: Fo) : (GPR axs ctx A)->(GPR axs ctx (A --> B))
             ->(GPR axs ctx B).
Definition APR := GPR axs0.
Definition p2_23_a ctx (t:Terms) : APR ctx (t == t).
apply MP with (A:=(t == t)).
change (Atom [t; t]) with ((t==t)).  (* <-- I don't want to write this line. *)

标签： coq

Answer 1

改变

Notation "( a '==' b )" := (Atom [a:Terms; b:Terms]).

到

Notation "( a '==' b )" := (Atom [a; b]).

类型注释出现在 AST 中，并且很容易被简化，因此符号很少匹配。