git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1076 from sellout/master

Filled in a couple missing lib pieces.

commit6e67f8ba583966b40f5a18730e1e451cb3c1435e authorEdwin Brady <edwin.brady@gmail.com> dateSun 20 Apr 2014, 16:27 (13 years ago) parentcfe250afc8da5f
2 files changed+14−3
compare with master
unifiedsplit
libs/prelude/Prelude/Classes.idr+8−2 libs/prelude/Prelude/Fin.idr+6−1
libs/prelude/Prelude/Classes.idr+8−2
@@ -244,14 +244,20 @@ instance Ord Bits64 where
244244
245245-- ------------------------------------------------------------- [ Bounded ]
246246
247−class MinBound b where
247+class Ord b => MinBound b where
248248 ||| The lower bound for the type
249249 minBound : b
250250
251−class MaxBound b where
251+class Ord b => MaxBound b where
252252 ||| The upper bound for the type
253253 maxBound : b
254254
255+instance MinBound Bits8 where
256+ minBound = 0x0
257+
258+instance MaxBound Bits8 where
259+ maxBound = 0xff
260+
255261instance MinBound Bits16 where
256262 minBound = 0x0
257263
libs/prelude/Prelude/Fin.idr+6−1
@@ -92,7 +92,12 @@ last {n=S _} = fS last
9292total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
9393fSinjective refl = refl
9494
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+
96101instance MinBound (Fin (S n)) where
97102 minBound = fZ
98103