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