CHANGELOG and doc updates for unary negation
commit9b51ca671a91d2bb7b78e70d44ff0abe76b2d645
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateMon 22 Sep 2014, 17:08 (12 years ago)
parent35d9a24
CHANGELOG+4
@@ -12,6 +12,10 @@ New in 0.9.15:
1212* More efficient representation of proof state, leading to faster elaboration
1313 of large expressions.
1414* EXPERIMENTAL Implementation of uniqueness types
15+* Unary negation now desugars to "negate", which is a method of the Neg type class.
16+ This allows instances of Num that can't be negative, like Nat, and it makes correct
17+ IEEE Float operations easier to encode. Additionally, unary negation is now available
18+ to DSL authors.
1519
1620New in 0.9.14:
1721--------------
libs/prelude/Prelude/Classes.idr+2−2
@@ -138,9 +138,9 @@ instance (Ord a, Ord b) => Ord (a, b) where
138138 else compare xr yr
139139
140140-- --------------------------------------------------------- [ Negatable Class ]
141−||| The Negatable class defines a typeclass for which negation works.
142−||| This is used for implementing unary -
141+||| The `Neg` class defines unary negation (-).
143142class Neg a where
143+ ||| The underlying implementation of unary minus. `-5` desugars to `negate (fromInteger 5)`.
144144 negate : a -> a
145145
146146instance Neg Integer where