git.iko.soy/Idris-dev
on master help sign in
extend Data.Sign
3505a60Alex Gryzlov
libs/contrib/Data/Sign.idr+29
compare with master
unifiedsplit
@@ -5,6 +5,35 @@ module Data.Sign
5||| A representation of signs for signed datatypes such as `ZZ`
5||| A representation of signs for signed datatypes such as `ZZ`
6data Sign = Plus | Zero | Minus
6data Sign = Plus | Zero | Minus
7
7
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+
8||| Discover the sign of some type
19||| Discover the sign of some type
9interface Signed t where
20interface Signed t where
10 total sign : t -> Sign
21 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