on master help sign in
Split Bounded into lower and upper bound type classes
commitea98726b017523a838854730a37c51f0102ccc79 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 21 Feb 2014, 14:56 (13 years ago) parent5c1d757
3 files changed+18−12
libs/prelude/Prelude/Classes.idr+12−11 libs/prelude/Prelude/Fin.idr+3−1 libs/prelude/Prelude/Nat.idr+3
libs/prelude/Prelude/Classes.idr+12−11
@@ -244,29 +244,30 @@ instance Ord Bits64 where
244244
245245-- ------------------------------------------------------------- [ Bounded ]
246246
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
251248 -- | The lower bound for the type
252249 minBound : b
250+
251+class MaxBound b where
253252 -- | The upper bound for the type
254253 maxBound : b
255254
256−instance Bounded () where
257− minBound = ()
258− maxBound = ()
259−
260−instance Bounded Bits16 where
255+instance MinBound Bits16 where
261256 minBound = 0x0
257+
258+instance MaxBound Bits16 where
262259 maxBound = 0xffff
263260
264−instance Bounded Bits32 where
261+instance MinBound Bits32 where
265262 minBound = 0x0
263+
264+instance MaxBound Bits32 where
266265 maxBound = 0xffffffff
267266
268−instance Bounded Bits64 where
267+instance MinBound Bits64 where
269268 minBound = 0x0
269+
270+instance MaxBound Bits64 where
270271 maxBound = 0xffffffffffffffff
271272
272273
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'
6161fSinjective refl = refl
6262
6363
64−instance Bounded (Fin (S n)) where
64+instance MinBound (Fin (S n)) where
6565 minBound = fZ
66+
67+instance MaxBound (Fin (S n)) where
6668 maxBound = last
6769
6870
libs/prelude/Prelude/Nat.idr+3
@@ -142,6 +142,9 @@ instance Num Nat where
142142
143143 fromInteger = fromIntegerNat
144144
145+instance MinBound Nat where
146+ minBound = Z
147+
145148instance Cast Integer Nat where
146149 cast = fromInteger
147150