From ce6465e279be4881d9097d409401c1e0d96d8083 Mon Sep 17 00:00:00 2001 From: Aaron Lebahn Date: Tue, 5 Jan 2021 07:56:04 -0600 Subject: [PATCH] Add public export to types/functions in Data.Fin.Order --- libs/base/Data/Fin/Order.idr | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/libs/base/Data/Fin/Order.idr b/libs/base/Data/Fin/Order.idr index ce02034ed..473f29bf0 100644 --- a/libs/base/Data/Fin/Order.idr +++ b/libs/base/Data/Fin/Order.idr @@ -10,23 +10,29 @@ import Decidable.Decidable import Decidable.Order using (k : Nat) + + public export data FinLTE : Fin k -> Fin k -> Type where FromNatPrf : {m, n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n + public export implementation Preorder (Fin k) FinLTE where transitive m n o (FromNatPrf p1) (FromNatPrf p2) = FromNatPrf (LTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2) reflexive n = FromNatPrf (LTEIsReflexive (finToNat n)) + public export implementation Poset (Fin k) FinLTE where antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) = finToNatInjective m n (LTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2) + public export implementation Decidable 2 [Fin k, Fin k] FinLTE where decide m n with (decideLTE (finToNat m) (finToNat n)) decide m n | Yes prf = Yes (FromNatPrf prf) decide m n | No disprf = No (\ (FromNatPrf prf) => disprf prf) + public export implementation Ordered (Fin k) FinLTE where order m n = either (Left . FromNatPrf)