aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/5522.v
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.