在Coq中找到像++这样的定义和符号

Question

我们怎样才能像那些符号的定义/类型"+",或"++"的List？

我曾尝试:Search ++,Search "++",Search (++), SearchAbout ...和 Check ++,Check "++",Check(++).

然而,他们都没有工作......

SearchAbout "++"确实显示了一些信息,但没有显示"++".

Answer 1

做:

Locate "++".

查找符号.

然后你可以Print/ Check表示实际的术语.

Answer 2

除了之前的答案,您可以使用Unfold "++"展开它的定义而无需先找到它.

例:

Coq < Goal forall A (l : list A), l ++ [] = [].
1 subgoal

  ============================
   forall (A : Type) (l : list A), l ++ [] = []

Unnamed_thm < unfold "++".
1 subgoal

  ============================
   forall (A : Type) (l : list A),
   (fix app (l0 m : list A) {struct l0} : list A :=
      match l0 with
      | [] => m
      | a :: l1 => a :: app l1 m
      end) l [] = []