];
binder: [
[ SYMBOL <:unicode<Pi>> (* Π *) -> `Pi
-(* | SYMBOL <:unicode<exists>> |+ ∃ +| -> `Exists *)
| SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
| SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
]
[
[ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19" ->
return_term loc (fold_cluster b vars typ body)
- | SYMBOL <:unicode<exists>> (* ∃ *);
- (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19"->
- return_term loc (fold_exists vars typ body)
]
];
term: LEVEL "70"