Найдите определение и обозначения как ++ в 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 [] = []