21

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 "++".

2 Answers 2

26

Do:

Locate "++".

To lookup for notations.

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

4
  • Thanks, this is very useful. But I'm still wondering is there a convenient command to do this in emacs & proof general ? Sep 29, 2018 at 6:59
  • @luochen1990 In ProofGeneral, the default shortcuts are C-c C-a C-c for Check, and C-c C-a C-p for Print. If you use menus, they are somewhere in the ProofGeneral menus too.
    – Ptival
    Sep 29, 2018 at 17:01
  • Thanks, but is there a shortcut for "Locate" ? Oct 9, 2018 at 2:52
  • Shortcut for Locate is C-c C-a C-n
    – lelf
    Jun 24, 2019 at 16:56
8

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 [] = []
2
  • Nit: presumably you meant l ++ [] = l, not l ++ [] = []? Sep 27, 2014 at 7:48
  • @MarkDickinson that would make it provable, yes. :)
    – sinan
    Sep 27, 2014 at 17:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.