Finden Sie die Definition und Notationen wie ++ in Coq

Question

Wie können wir die Definition/Typ für diese Bezeichnungen wie "+" oder "++" von List bekommen?

ich versucht habe: Search ++, Search "++", Search (++), SearchAbout ... und Check ++, Check "++", Check(++).

Keiner von ihnen jedoch arbeiten ...

SearchAbout "++" einige Informationen nicht zeigt, aber nicht die Definition von "++".

Answer 1

Sie:

Locate "++". 

für Notationen Lookup.

Dann können Sie Print/Check den tatsächlichen Begriff bezeichnet werden.

Answer 2

Zusätzlich zur vorherigen Antwort können Sie Unfold "++" verwenden, um seine Definition zu entfalten, ohne sie zuerst zu finden.

Beispiel:

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 [] = []