Find the definition and notations like ++ in Coq

Question

How can we get the definition/type for those notations like "+", or "++" of List?

I have tried : Search ++, Search "++", Search (++), SearchAbout ... and Check ++, Check "++", Check(++).

None of them work however...

SearchAbout "++" does show some info, but not the definition of "++".

Answer 1

Do:

Locate "++".

To lookup for notations.

Then you can Print/Check the actual term being denoted.

Answer 2

In addition to previous answer, you can use Unfold "++" to unfold it's definition without locating it first.

Example:

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