Hi folks,

I have this code

```
Inductive Add nat : Type :=
| id : nat -> Add nat
| add : Add nat -> nat -> Add nat.
Arguments id {_}.
Arguments add {_}.
Check id 1.
Check add (id 1) 1.
Check add (add (id 1) 1) 1.
Declare Custom Entry expr.
Notation "[ e ]" := e (e custom expr at level 2).
Notation "0" := (id 0) (in custom expr at level 0).
Notation "x + y" := (add x y) (in custom expr at level 2, left associativity).
Notation "x" := x (in custom expr at level 0, x ident).
Notation "{ x }" := x (in custom expr, x constr).
Unset Printing Notations.
Check [0 + {1} + {2}].
Set Printing Notations.
Fixpoint interp (s : Add nat) : nat :=
match s with
| id n => n
| add s' n => interp s' + n
end.
Eval simpl in interp ([0 + {1} + {2} + {3}]).
```

I'm looking for a way to get rid of `0`

in `[0 + {1} + {2}]`

and also looking for a way to get rid of the braces, I mean, be able to do this `[1 + 2 + 3]`

instead of `[0 + {1} + {2} + {3]]`

.

Last updated: Jan 28 2023 at 06:30 UTC