blob: 66cd6dfa8c56b6d907b0191dcf2f9484d893d209 (
plain)
1
2
3
4
5
|
(* Was generating a dangling "pat" variable at some time *)
Notation "'plet' x := e 'in' t" :=
((fun H => let x := id H in t) e) (at level 0, x pattern).
Definition bla := plet (pair x y) := pair 1 2 in x.
|