git.iko.soy/Idris-dev
on master help sign in
Some trivial renamings
75e34a7Edwin Brady
libs/contrib/Data/ZZ.idr+2−2
compare with master
unifiedsplit
@@ -68,8 +68,8 @@ multZ (Pos n) (NegS m) = negNat $ n * (S m)
68||| Convert an `Integer` to an inductive representation.
68||| Convert an `Integer` to an inductive representation.
69fromInt : Integer -> ZZ
69fromInt : Integer -> ZZ
70fromInt n = if n < 0
70fromInt n = if n < 0
71− then NegS $ fromInteger {a=Nat} ((-n) - 1)
71+ then NegS $ fromInteger ((-n) - 1)
72− else Pos $ fromInteger {a=Nat} n
72+ else Pos $ fromInteger n
73
73
74implementation Cast Nat ZZ where
74implementation Cast Nat ZZ where
75 cast n = Pos n
75 cast n = Pos n
libs/prelude/Prelude/Algebra.idr+4−4
@@ -15,8 +15,8 @@ infixl 6 <+>
15|||
15|||
16||| + Associativity of `<+>`:
16||| + Associativity of `<+>`:
17||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
17||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
18−interface Semigroup a where
18+interface Semigroup ty where
19− (<+>) : a -> a -> a
19+ (<+>) : ty -> ty -> ty
20
20
21
21
22||| Sets equipped with a single binary operation that is associative, along with
22||| Sets equipped with a single binary operation that is associative, along with
@@ -28,6 +28,6 @@ interface Semigroup a where
28||| + Neutral for `<+>`:
28||| + Neutral for `<+>`:
29||| forall a, a <+> neutral == a
29||| forall a, a <+> neutral == a
30||| forall a, neutral <+> a == a
30||| forall a, neutral <+> a == a
31−interface Semigroup a => Monoid a where
31+interface Semigroup ty => Monoid ty where
32− neutral : a
32+ neutral : ty
33
33
libs/prelude/Prelude/Classes.idr+25−25
@@ -21,9 +21,9 @@ boolOp op x y = intToBool (op x y)
21
21
22-- ---------------------------------------------------------- [ Equality Interface ]
22-- ---------------------------------------------------------- [ Equality Interface ]
23||| The Eq interface defines inequality and equality.
23||| The Eq interface defines inequality and equality.
24−interface Eq a where
24+interface Eq ty where
25− (==) : a -> a -> Bool
25+ (==) : ty -> ty -> Bool
26− (/=) : a -> a -> Bool
26+ (/=) : ty -> ty -> Bool
27
27
28 x /= y = not (x == y)
28 x /= y = not (x == y)
29 x == y = not (x /= y)
29 x == y = not (x /= y)
@@ -78,29 +78,29 @@ thenCompare EQ y = y
78thenCompare GT y = GT
78thenCompare GT y = GT
79
79
80||| The Ord interface defines comparison operations on ordered data types.
80||| The Ord interface defines comparison operations on ordered data types.
81−interface Eq a => Ord a where
81+interface Eq ty => Ord ty where
82− compare : a -> a -> Ordering
82+ compare : ty -> ty -> Ordering
83
83
84− (<) : a -> a -> Bool
84+ (<) : ty -> ty -> Bool
85 (<) x y with (compare x y)
85 (<) x y with (compare x y)
86 (<) x y | LT = True
86 (<) x y | LT = True
87 (<) x y | _ = False
87 (<) x y | _ = False
88
88
89− (>) : a -> a -> Bool
89+ (>) : ty -> ty -> Bool
90 (>) x y with (compare x y)
90 (>) x y with (compare x y)
91 (>) x y | GT = True
91 (>) x y | GT = True
92 (>) x y | _ = False
92 (>) x y | _ = False
93
93
94− (<=) : a -> a -> Bool
94+ (<=) : ty -> ty -> Bool
95 (<=) x y = x < y || x == y
95 (<=) x y = x < y || x == y
96
96
97− (>=) : a -> a -> Bool
97+ (>=) : ty -> ty -> Bool
98 (>=) x y = x > y || x == y
98 (>=) x y = x > y || x == y
99
99
100− max : a -> a -> a
100+ max : ty -> ty -> ty
101 max x y = if x > y then x else y
101 max x y = if x > y then x else y
102
102
103− min : a -> a -> a
103+ min : ty -> ty -> ty
104 min x y = if (x < y) then x else y
104 min x y = if (x < y) then x else y
105
105
106Ord () where
106Ord () where
@@ -151,11 +151,11 @@ Ord Bool where
151
151
152-- --------------------------------------------------------- [ Numerical Interface ]
152-- --------------------------------------------------------- [ Numerical Interface ]
153||| The Num interface defines basic numerical arithmetic.
153||| The Num interface defines basic numerical arithmetic.
154−interface Num a where
154+interface Num ty where
155− (+) : a -> a -> a
155+ (+) : ty -> ty -> ty
156− (*) : a -> a -> a
156+ (*) : ty -> ty -> ty
157 ||| Conversion from Integer.
157 ||| Conversion from Integer.
158− fromInteger : Integer -> a
158+ fromInteger : Integer -> ty
159
159
160Num Integer where
160Num Integer where
161 (+) = prim__addBigInt
161 (+) = prim__addBigInt
@@ -198,12 +198,12 @@ Num Bits64 where
198
198
199-- --------------------------------------------------------- [ Negatable Interface ]
199-- --------------------------------------------------------- [ Negatable Interface ]
200||| The `Neg` interface defines operations on numbers which can be negative.
200||| The `Neg` interface defines operations on numbers which can be negative.
201−interface Num a => Neg a where
201+interface Num ty => Neg ty where
202 ||| The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.
202 ||| The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.
203− negate : a -> a
203+ negate : ty -> ty
204− (-) : a -> a -> a
204+ (-) : ty -> ty -> ty
205 ||| Absolute value
205 ||| Absolute value
206− abs : a -> a
206+ abs : ty -> ty
207
207
208Neg Integer where
208Neg Integer where
209 negate x = prim__subBigInt 0 x
209 negate x = prim__subBigInt 0 x
@@ -306,9 +306,9 @@ MaxBound Bits64 where
306
306
307-- ------------------------------------------------------------- [ Fractionals ]
307-- ------------------------------------------------------------- [ Fractionals ]
308
308
309−interface Num a => Fractional a where
309+interface Num ty => Fractional ty where
310− (/) : a -> a -> a
310+ (/) : ty -> ty -> ty
311− recip : a -> a
311+ recip : ty -> ty
312
312
313 recip x = 1 / x
313 recip x = 1 / x
314
314
@@ -318,9 +318,9 @@ Fractional Double where
318-- --------------------------------------------------------------- [ Integrals ]
318-- --------------------------------------------------------------- [ Integrals ]
319%default partial
319%default partial
320
320
321−interface Num a => Integral a where
321+interface Num ty => Integral ty where
322− div : a -> a -> a
322+ div : ty -> ty -> ty
323− mod : a -> a -> a
323+ mod : ty -> ty -> ty
324
324
325-- ---------------------------------------------------------------- [ Integers ]
325-- ---------------------------------------------------------------- [ Integers ]
326divBigInt : Integer -> Integer -> Integer
326divBigInt : Integer -> Integer -> Integer
libs/prelude/Prelude/Interactive.idr+4−4
@@ -46,20 +46,20 @@ putStrLn = putStrLn'
46
46
47||| Output something showable to stdout, without a trailing newline, for any FFI
47||| Output something showable to stdout, without a trailing newline, for any FFI
48||| descriptor
48||| descriptor
49−print' : Show a => a -> IO' ffi ()
49+print' : Show ty => ty -> IO' ffi ()
50print' x = putStr' (show x)
50print' x = putStr' (show x)
51
51
52||| Output something showable to stdout, without a trailing newline
52||| Output something showable to stdout, without a trailing newline
53−print : Show a => a -> IO ()
53+print : Show ty => ty -> IO ()
54print = print'
54print = print'
55
55
56||| Output something showable to stdout, with a trailing newline, for any FFI
56||| Output something showable to stdout, with a trailing newline, for any FFI
57||| descriptor
57||| descriptor
58−printLn' : Show a => a -> IO' ffi ()
58+printLn' : Show ty => ty -> IO' ffi ()
59printLn' x = putStrLn' (show x)
59printLn' x = putStrLn' (show x)
60
60
61||| Output something showable to stdout, with a trailing newline
61||| Output something showable to stdout, with a trailing newline
62−printLn : Show a => a -> IO ()
62+printLn : Show ty => ty -> IO ()
63printLn = printLn'
63printLn = printLn'
64
64
65||| Read one line of input from stdin, without the trailing newline, for any FFI
65||| Read one line of input from stdin, without the trailing newline, for any FFI
libs/prelude/Prelude/Show.idr+5−5
@@ -38,12 +38,12 @@ Ord Prec where
38 compare x y = compare (precCon x) (precCon y)
38 compare x y = compare (precCon x) (precCon y)
39
39
40||| Things that have a canonical `String` representation.
40||| Things that have a canonical `String` representation.
41−interface Show a where
41+interface Show ty where
42 ||| Convert a value to its `String` representation.
42 ||| Convert a value to its `String` representation.
43 |||
43 |||
44− ||| @ a the value to convert
44+ ||| @ x the value to convert
45 partial
45 partial
46− show : (x : a) -> String
46+ show : (x : ty) -> String
47 show = showPrec Open
47 show = showPrec Open
48
48
49 ||| Convert a value to its `String` representation in a certain precedence
49 ||| Convert a value to its `String` representation in a certain precedence
@@ -58,9 +58,9 @@ interface Show a where
58 ||| their own bracketing, like `Pair` and `List`.
58 ||| their own bracketing, like `Pair` and `List`.
59 |||
59 |||
60 ||| @ d the precedence context.
60 ||| @ d the precedence context.
61− ||| @ a the value to convert
61+ ||| @ x the value to convert
62 partial
62 partial
63− showPrec : (d : Prec) -> (x : a) -> String
63+ showPrec : (d : Prec) -> (x : ty) -> String
64 showPrec _ = show
64 showPrec _ = show
65
65
66||| Surround a `String` with parentheses depending on a condition.
66||| Surround a `String` with parentheses depending on a condition.