Give Fin an Ord instance.
commit6f651b0a1bfae86caf73d04fe2cd3833c70dff71
authorGreg Pfeil <greg@technomadic.org>
dateThu 17 Apr 2014, 15:12 (13 years ago)
parent272b5a5
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