Stream: Coq users

Topic: Creating custom entry


view this post on Zulip Julin S (Dec 23 2021 at 05:45):

Hi. I was trying to make a notation within a custom entry like

Inductive binop : Set := Plus | Mult.

Inductive exp : Set :=
| Const : nat -> exp
| Binop : binop -> exp -> exp -> exp.

(* Make custom entry and notations *)
Declare Custom Entry expr.
Notation "'{{' e '}}'" := (e) (e custom expr at level 100).
Notation "a + b" := (Plus (Const a) (Const b)) (in custom expr at level 10, left associativity).

(* Without the notation. ✓ *)
Compute Binop Plus (Const 3) (Const 4).

(* Trying with the notation. ✗ *)
Compute {{ 3 + 4 }}.
(* Syntax error: [constr:expr level 100] expected after '{{' (in [constr:operconstr]). *)

What am I doing wrong here?

How can I make {{ 3 + 4 }} equivalent of Binop Plus (Const 3) (Const 4)?

view this post on Zulip Paolo Giarrusso (Dec 23 2021 at 10:18):

What if you move + to level 100?

view this post on Zulip Gaëtan Gilbert (Dec 23 2021 at 10:19):

3 and 4 aren't in expr is the issue afaict


Last updated: Feb 04 2023 at 23:02 UTC