- term: LEVEL "10" (* let in *)
- [ "10" NONA
- [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
- p1 = term; "in"; p2 = term ->
- return_term loc (LetIn (var, p1, p2))
- | "let"; k = induction_kind; defs = let_defs; "in";
- body = term ->
- return_term loc (LetRec (k, defs, body))
- ]
- ];
- term: LEVEL "20" (* binder *)
- [ "20" RIGHTA
+ term: LEVEL "10N" [ (* let in *)
+ [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
+ p1 = term; "in"; p2 = term ->
+ return_term loc (LetIn (var, p1, p2))
+ | "let"; k = induction_kind; defs = let_defs; "in";
+ body = term ->
+ return_term loc (LetRec (k, defs, body))
+ ]
+ ];
+ term: LEVEL "20R" (* binder *)
+ [