diff options
Diffstat (limited to 'src/Data/Fin/Strong.idr')
| -rw-r--r-- | src/Data/Fin/Strong.idr | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/Data/Fin/Strong.idr b/src/Data/Fin/Strong.idr index ebf3483..a0ed5df 100644 --- a/src/Data/Fin/Strong.idr +++ b/src/Data/Fin/Strong.idr @@ -1,6 +1,8 @@ module Data.Fin.Strong import Data.Fin +import Decidable.Equality.Core +import Syntax.PreorderReasoning public export data SFin : Nat -> Type where @@ -61,6 +63,14 @@ Injective (FS' {n}) where injective {x = FS x, y = FS y} prf = cong FS $ injective {f = FS'} $ injective prf export +Injective (strongToFin {n}) where + injective {x, y} prf = Calc $ + |~ x + ~~ finToStrong (strongToFin x) ..<(strongToFinToStrong x) + ~~ finToStrong (strongToFin y) ...(cong finToStrong prf) + ~~ y ...(strongToFinToStrong y) + +export Uninhabited (SFin 0) where uninhabited x impossible export @@ -74,3 +84,9 @@ sucNonZero (FS x) prf = absurd prf export sucIsFS : (x : SFin (S n)) -> FS' x = FS x sucIsFS x = rewrite strongToFinToStrong x in Refl + +export +DecEq (SFin n) where + decEq x y = viaEquivalence + (MkEquivalence (injective {f = strongToFin}) (\prf => cong strongToFin prf)) + (decEq (strongToFin x) (strongToFin y)) |