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)`

?

What if you move + to level 100?

3 and 4 aren't in `expr`

is the issue afaict

Last updated: Oct 05 2023 at 02:01 UTC