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}]).