blob: 40627e331ec9e5cb2b4626bff0e1b3db7745080f (
plain)
1
2
3
4
5
6
7
8
|
(* Was failing at printing time with stack overflow due to an infinite
eta-expansion *)
Notation "x 'where' y .. z := v " :=
((fun y => .. ((fun z => x) v) ..) v)
(at level 11, v at next level, y binder, z binder).
Check forall f, f x where x := 1.
|
