Предотвратить непреднамеренное развертывание после применения в Coq - PullRequest
Новая
       6

Предотвратить непреднамеренное развертывание после применения в Coq

0 голосов
/ 24 сентября 2018

Моя запись была непреднамеренно развернута после применения.Я не хочу называть тактику «изменение» в последней строке текста крошечного примера каждый раз, когда использую modus ponens.Как запретить Coq раскрывать мою нотацию "(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. *)

1 Ответ

0 голосов
/ 24 сентября 2018

Изменить 

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

на 

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

Типовые аннотации появляются в AST и их легко упростить, поэтому обозначения редко совпадают.

...