git.iko.soy/Idris-dev
on master help sign in
CHANGELOG and doc updates for unary negation
9b51ca6David Raymond Christiansen
CHANGELOG+4
compare with master
unifiedsplit
@@ -12,6 +12,10 @@ New in 0.9.15:
12* More efficient representation of proof state, leading to faster elaboration
12* More efficient representation of proof state, leading to faster elaboration
13 of large expressions.
13 of large expressions.
14* EXPERIMENTAL Implementation of uniqueness types
14* 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.
15
19
16New in 0.9.14:
20New in 0.9.14:
17--------------
21--------------
libs/prelude/Prelude/Classes.idr+2−2
@@ -138,9 +138,9 @@ instance (Ord a, Ord b) => Ord (a, b) where
138 else compare xr yr
138 else compare xr yr
139
139
140-- --------------------------------------------------------- [ Negatable Class ]
140-- --------------------------------------------------------- [ Negatable Class ]
141−||| The Negatable class defines a typeclass for which negation works.
141+||| The `Neg` class defines unary negation (-).
142−||| This is used for implementing unary -
143class Neg a where
142class Neg a where
143+ ||| The underlying implementation of unary minus. `-5` desugars to `negate (fromInteger 5)`.
144 negate : a -> a
144 negate : a -> a
145
145
146instance Neg Integer where
146instance Neg Integer where