Software Foundations '| -' обозначение теней Обозначение соответствия Ltac

Question

Software Foundations использует |- в нескольких своих обозначениях. Так, например, в Stlc:

Reserved Notation "Gamma '|-' t '\in' T" (at level 40). 

Это мешает конструкции матча Ltac. Например, это:

Ltac test := 
    match goal with 
    H: _ |- _ => idtac 
    end. 

отлично работает за пределами Stlc, но после того, что обозначение определено, оно терпит неудачу с:

Toplevel input, characters 43-44: 
Syntax error: "\in" expected after [constr:operconstr level 200] (in [constr:operconstr]). 

Есть что-нибудь, что можно сделать, кроме изменения Gamma '|-' t '\in' T обозначения ?

Answer 1

Насколько я знаю, нет ничего, что можно сделать здесь, чтобы действительно устранить проблему. Расширяемый синтаксический анализатор Coq очень хрупкий, и подобные конфликты могут привести к тому, что некоторые вещи станут непревзойденными.

Обойти это объявить обозначения в модуле:

(* Foo.v *) 
Module MyNotation. 

Reserved Notation "Gamma '|-' t '\in' T" (at level 40). 

(* Include actual notation definition somewhere here *) 

End MyNotation. 

Чтобы использовать обозначения, просто импортировать модуль:

(* Bar.v *) 
Require Import Foo. 

Import MyNotation. 

Definition asdf := 4. 

Затем вы можете использовать Foo и Bar в другом месте, не имея обозначение конфликта с кодом ltac:

(* Baz.v *) 
Require Import Foo. 
Require Import Bar. 

Ltac test := 
    match goal with 
    | H : _ |- _ => idtac 
    end.