软件基础阴影Ltac匹配符号

Question

软件基础在几个符号中使用了|-。例如，在斯泰克中

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.