@@ -127,6 +127,11 @@ using (k : Nat)
127 instance Poset (Fin k) FinLTE where
127 instance Poset (Fin k) FinLTE where
128 antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =
128 antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =
129 finToNatInjective m n (NatLTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)
129 finToNatInjective m n (NatLTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)
131+ instance Decidable [Fin k, Fin k] FinLTE where
132+ decide m n with (decideNatLTE (finToNat m) (finToNat n))
133+ | Yes prf = Yes (FromNatPrf prf)
134+ | No disprf = No (\ (FromNatPrf prf) => disprf prf)
131 instance Ordered (Fin k) FinLTE where
136 instance Ordered (Fin k) FinLTE where
132 order m n =
137 order m n =