Tìm định nghĩa và ký hiệu như ++ trong Coq

Question

Làm cách nào chúng tôi có thể nhận định nghĩa/loại cho các ký hiệu như "+" hoặc "++" của List?

Tôi đã thử: Search ++, Search "++", Search (++), SearchAbout ... và Check ++, Check "++", Check(++).

Không ai trong số họ làm việc tuy nhiên ...

SearchAbout "++" không hiển thị một số thông tin, nhưng không phải là định nghĩa của "++".

Answer 1

Do:

Locate "++". 

Để tra cứu cho ký hiệu.

Sau đó, bạn có thể Print/Check cụm từ thực tế được biểu thị.

Answer 2

Ngoài câu trả lời trước, bạn có thể sử dụng Unfold "++" để mở định nghĩa của nó mà không định vị trước.

Ví dụ:

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