on master help sign in
Split Bounded into lower and upper bound type classes
ea98726David Raymond Christiansen
libs/prelude/Prelude/Classes.idr+12−11
@@ -244,29 +244,30 @@ instance Ord Bits64 where
244
244
245-- ------------------------------------------------------------- [ Bounded ]
245-- ------------------------------------------------------------- [ Bounded ]
246
246
247−-- | Names the upper and lower elements of a type. Ord is not a superclass of
248−-- Bounded since types that are not totally ordered may also have upper and
249−-- lower bounds.
250−class Bounded b where
247+class MinBound b where
251 -- | The lower bound for the type
248 -- | The lower bound for the type
252 minBound : b
249 minBound : b
250+
251+class MaxBound b where
253 -- | The upper bound for the type
252 -- | The upper bound for the type
254 maxBound : b
253 maxBound : b
255
254
256−instance Bounded () where
257− minBound = ()
258− maxBound = ()
259−
260−instance Bounded Bits16 where
255+instance MinBound Bits16 where
261 minBound = 0x0
256 minBound = 0x0
257+
258+instance MaxBound Bits16 where
262 maxBound = 0xffff
259 maxBound = 0xffff
263
260
264−instance Bounded Bits32 where
261+instance MinBound Bits32 where
265 minBound = 0x0
262 minBound = 0x0
263+
264+instance MaxBound Bits32 where
266 maxBound = 0xffffffff
265 maxBound = 0xffffffff
267
266
268−instance Bounded Bits64 where
267+instance MinBound Bits64 where
269 minBound = 0x0
268 minBound = 0x0
269+
270+instance MaxBound Bits64 where
270 maxBound = 0xffffffffffffffff
271 maxBound = 0xffffffffffffffff
271
272
272
273
libs/prelude/Prelude/Fin.idr+3−1
@@ -61,8 +61,10 @@ total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
61fSinjective refl = refl
61fSinjective refl = refl
62
62
63
63
64−instance Bounded (Fin (S n)) where
64+instance MinBound (Fin (S n)) where
65 minBound = fZ
65 minBound = fZ
66+
67+instance MaxBound (Fin (S n)) where
66 maxBound = last
68 maxBound = last
67
69
68
70
libs/prelude/Prelude/Nat.idr+3
@@ -142,6 +142,9 @@ instance Num Nat where
142
142
143 fromInteger = fromIntegerNat
143 fromInteger = fromIntegerNat
144
144
145+instance MinBound Nat where
146+ minBound = Z
147+
145instance Cast Integer Nat where
148instance Cast Integer Nat where
146 cast = fromInteger
149 cast = fromInteger
147
150