@@ -5,6 +5,35 @@ module Data.Sign
55||| A representation of signs for signed datatypes such as `ZZ`
66data Sign = Plus | Zero | Minus
77
8+opposite : Sign -> Sign
9+opposite Plus = Minus
10+opposite Zero = Zero
11+opposite Minus = Plus
12+
13+multiply : Sign -> Sign -> Sign
14+multiply Zero _ = Zero
15+multiply _ Zero = Zero
16+multiply Plus x = x
17+multiply Minus x = opposite x
18+
819||| Discover the sign of some type
920interface Signed t where
1021 total sign : t -> Sign
22+
23+Signed Int where
24+ sign x with (compare x 0)
25+ | LT = Minus
26+ | EQ = Zero
27+ | GT = Plus
28+
29+Signed Integer where
30+ sign x with (compare x 0)
31+ | LT = Minus
32+ | EQ = Zero
33+ | GT = Plus
34+
35+Signed Double where
36+ sign x with (compare x 0.0)
37+ | LT = Minus
38+ | EQ = Zero
39+ | GT = Plus