blob: 0fae9ede4235a5b82817d44b5a7bb31f261974cf (
plain)
1
2
3
4
5
6
7
|
(* Checking support for scope delimiters and as clauses in 'pat
applied to notations with binders *)
Notation "'multifun' x .. y 'in' f" := (fun x => .. (fun y => f) .. )
(at level 200, x binder, y binder, f at level 200).
Check multifun '((x, y)%core as z) in (x+y,0)=z.
|
