git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1076 from sellout/master
6e67f8bEdwin Brady
libs/prelude/Prelude/Classes.idr+8−2
compare with master
unifiedsplit
@@ -244,14 +244,20 @@ instance Ord Bits64 where
244
244
245-- ------------------------------------------------------------- [ Bounded ]
245-- ------------------------------------------------------------- [ Bounded ]
246
246
247−class MinBound b where
247+class Ord b => MinBound b where
248 ||| The lower bound for the type
248 ||| The lower bound for the type
249 minBound : b
249 minBound : b
250
250
251−class MaxBound b where
251+class Ord b => MaxBound b where
252 ||| The upper bound for the type
252 ||| The upper bound for the type
253 maxBound : b
253 maxBound : b
254
254
255+instance MinBound Bits8 where
256+ minBound = 0x0
257+
258+instance MaxBound Bits8 where
259+ maxBound = 0xff
260+
255instance MinBound Bits16 where
261instance MinBound Bits16 where
256 minBound = 0x0
262 minBound = 0x0
257
263
libs/prelude/Prelude/Fin.idr+6−1
@@ -92,7 +92,12 @@ last {n=S _} = fS last
92total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
92total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
93fSinjective refl = refl
93fSinjective refl = refl
94
94
95−
95+instance Ord (Fin n) where
96+ compare fZ fZ = EQ
97+ compare fZ (fS _) = LT
98+ compare (fS _) fZ = GT
99+ compare (fS x) (fS y) = compare x y
100+
96instance MinBound (Fin (S n)) where
101instance MinBound (Fin (S n)) where
97 minBound = fZ
102 minBound = fZ
98
103