Add impossible cases to CHANGELOG
commite9ea90d2a3d56edf5261f47adfa2f540e19403c5
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateTue 31 Mar 2015, 12:52 (12 years ago)
parente45c9b8
CHANGELOG+2
@@ -19,6 +19,8 @@ New in 0.9.18:
1919* Pattern-matching lambdas are allowed to be impossible. For example,
2020 Dec (2 = 3) can now be constructed with No $ \(Refl) impossible, instead of
2121 requiring a separate lemma.
22+* Case alternatives are allowed to be impossible:
23+ case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }
2224
2325New in 0.9.17:
2426--------------