Julin S (Dec 23 2021 at 05:45): 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)?
Paolo Giarrusso (Dec 23 2021 at 10:18):What if you move + to level 100?
Gaëtan Gilbert (Dec 23 2021 at 10:19):3 and 4 aren't in expr is the issue afaict
Last updated: Oct 05 2023 at 02:01 UTC