Added the Zero Constructor to Data.Sign
Added the Zero Constructor to Sign and adapted the ZZ instance
this addition.
commitcf25411a72fd4147e5fe604f5b9c6cad7f0c17ff
authorJakob Brünker <jakob.bruenker@gmail.com>
dateMon 9 Feb 2015, 23:59 (12 years ago)
parenta87f69e
libs/base/Data/Sign.idr+1−1
@@ -1,7 +1,7 @@
11module Data.Sign
22
33||| A representation of signs for signed datatypes such as `ZZ`
4−data Sign = Plus | Minus
4+data Sign = Plus | Zero | Minus
55
66||| Discover the sign of some type
77class Signed t where
libs/base/Data/ZZ.idr+1
@@ -15,6 +15,7 @@ import Data.Sign
1515data ZZ = Pos Nat | NegS Nat
1616
1717instance Signed ZZ where
18+ sign (Pos Z) = Zero
1819 sign (Pos _) = Plus
1920 sign (NegS _) = Minus
2021