Add pattern-matching lambdas to CHANGELOG
commite45c9b83565c7e563da34a696c9daf45d2d48a38
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateTue 31 Mar 2015, 12:36 (12 years ago)
parent7379574
CHANGELOG+3
@@ -16,6 +16,9 @@ New in 0.9.18:
1616* Syntax rules no longer perform variable capture. Users of effects will
1717 need to explicitly name results in dependent effect signatures instead
1818 of using the default name "result".
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
21+ requiring a separate lemma.
1922
2023New in 0.9.17:
2124--------------