Search code examples
coq

Locate a Notation that takes an infix argument

In the Coq.Numbers.Cyclic.ZModulo.ZModulo library, there is the following notation:

Notation "[+| c |]" :=
   (interp_carry 1 wB to_Z c) (at level 0, c at level 99).

How can I search this? I tried

Locate "[+| _ |]".  (* Unknown Notation *)
Locate "[+| |]".    (* Unknown Notation *)
Locate "[+| _ |]".  (* Unknown Notation *)
Locate "[+| c |]".  (* Unknown Notation *)
Locate "[+| ?c |]". (* Unknown Notation *)
Locate [+| ?c |].   (* Error: Syntax error: 'Ltac' or [locatable] expected after 'Locate' (in [vernac:command]). *)
Solution

  • Your first and fourth choices, Locate "[+| _ |]", Locate "[+| c |]". are both correct. Note that the variable name doesn't matter: you could do Locate "[+| abcdef |]". too.

    Note, however, that the particular notation you refer to is inside a section. This means that it's inaccessible outside the section. In particular, Locate won't find it. To test this, try this code:

    Section ZModulo.
  Notation "[+| c |]" := (S c).

  Locate "[+| _ |]".
  (* Notation
     "[+| c |]" := S c (default interpretation) *)

  Locate "[+| c |]".
  (* Notation
     "[+| c |]" := S c (default interpretation) *)

  Locate "[+| abcdef |]".
  (* Notation
     "[+| c |]" := S c (default interpretation) *)
End ZModulo.

Locate "[+| _ |]". (* Unknown notation *)
Locate "[+| c |]". (* Unknown notation *)
Locate "[+| abcdef |]". (* Unknown notation *)

    In versions of Coq earlier than 8.8.0, only the first version will work. In 8.8.0, Locate was updated to allow the other form.