Merge pull request #1902 from JakobBruenker/master
Added the Zero Constructor to Data.Sign
commit38e3a4083a016499b92d5fb4437aea1de242d3a8
authorDavid Christiansen <david@davidchristiansen.dk>
dateTue 10 Feb 2015, 16:32 (12 years ago)
parenta87f69ecf25411
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