Data.Fin.Order

Implementation  of ordering relations for `Fin`ite numbers

Definitions

data FinLTE : Fin k -> Fin k -> Type

Totality: total
Visibility: public export
Constructor: 

FromNatPrf : LTE (finToNat m) (finToNat n) -> FinLTE m n

Hints:

Antisymmetric (Fin k) FinLTE

Connex (Fin k) FinLTE

Decidable 2 [Fin k, Fin k] FinLTE

PartialOrder (Fin k) FinLTE

Preorder (Fin k) FinLTE

Reflexive (Fin k) FinLTE

Transitive (Fin k) FinLTE