@@ -19,6 +19,8 @@ New in 0.9.18:
19* Pattern-matching lambdas are allowed to be impossible. For example,
19* Pattern-matching lambdas are allowed to be impossible. For example,
20 Dec (2 = 3) can now be constructed with No $ \(Refl) impossible, instead of
20 Dec (2 = 3) can now be constructed with No $ \(Refl) impossible, instead of
21 requiring a separate lemma.
21 requiring a separate lemma.
22+* Case alternatives are allowed to be impossible:
23+ case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }
23New in 0.9.17:
25New in 0.9.17:
24--------------
26--------------