git.iko.soy/Idris-dev
on master help sign in
Added the Zero Constructor to Data.Sign
cf25411Jakob Brünker
libs/base/Data/Sign.idr+1−1
compare with master
unifiedsplit
@@ -1,7 +1,7 @@
1module Data.Sign
1module Data.Sign
2
2
3||| A representation of signs for signed datatypes such as `ZZ`
3||| A representation of signs for signed datatypes such as `ZZ`
4−data Sign = Plus | Minus
4+data Sign = Plus | Zero | Minus
5
5
6||| Discover the sign of some type
6||| Discover the sign of some type
7class Signed t where
7class Signed t where
libs/base/Data/ZZ.idr+1
@@ -15,6 +15,7 @@ import Data.Sign
15data ZZ = Pos Nat | NegS Nat
15data ZZ = Pos Nat | NegS Nat
16
16
17instance Signed ZZ where
17instance Signed ZZ where
18+ sign (Pos Z) = Zero
18 sign (Pos _) = Plus
19 sign (Pos _) = Plus
19 sign (NegS _) = Minus
20 sign (NegS _) = Minus
20
21