Stream: Coq users

Topic: Custom entry


view this post on Zulip Julin Shaji (Apr 27 2024 at 10:56):

I was trying to make a custom entry like this:

Require Import Bool.
Declare Custom Entry foo.
Notation "[ e ]" := e (e custom foo at level 2).
Notation "'<' b '>'" := (Bool.eqb b) (in custom foo at level 0, b constr).
(* Notation "( x )" := x (in custom foo, x at level 2). *)

Print Custom Grammar foo.
(*
Entry custom:foo is
[ "2" RIGHTA
  [  ]
| "0" RIGHTA
  [ "<"; term LEVEL "200"; ">" ] ]
*)

But it's not working out:

Check [ < true > ].
(*              ^^^

Syntax error: [term] expected after '>' (in [term]).

*)

Any idea what I'm doing wrong here?
I tried reading up the documentation page, but couldn't pinpoint it.

view this post on Zulip Julin Shaji (Apr 27 2024 at 11:03):


Oh, that got fixed by using at level 0

  Notation "'<' c '>'" := (Char (Bool.eqb c)) (in custom re at level 0, c constr at level 0).

I seem to be doing guesswork to get this right..


view this post on Zulip Julin Shaji (Apr 27 2024 at 11:56):

I was trying to have two notations within the custom entry: and
(both infix).
Such that has more precedence.

I tried:

Declare Custom Entry foo.
Notation "[ e ]" := e (e custom foo at level 2).
Notation "a '∧' b" := (and a b) (in custom foo at level 5, a constr at level 0, b constr at level 0).
Notation "a '∨' b" := (or a b) (in custom foo at level 10, a constr at level 0, b constr at level 0).

Check [True  False].

But this gave error:

Check [True  False].
(*         ^^^
Syntax error: '∨' expected after [term level 0] (in [custom:foo]).
*)

How can this be fixed?

view this post on Zulip Julin Shaji (Apr 27 2024 at 11:58):

Smaller the level, higher the precedence, right?

view this post on Zulip Julin Shaji (Apr 27 2024 at 15:47):

It seems to work all right outside custom entry:

Notation "a '∧' b" := (and a b) (at level 5).
Notation "a '∨' b" := (or a b) (at level 10).

Set Printing Parentheses.
Check False  True  False.
(* (False ∧ True) ∨ False : Prop *)

view this post on Zulip Julin Shaji (Apr 27 2024 at 15:57):

Perhaps looking at camlp5 docs might help in understanding how this works?


Last updated: Jun 23 2024 at 04:03 UTC