diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-14 17:47:22 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-14 17:47:22 +0100 |
| commit | ed9beabb1e5f867bad0c0693f36cd0ffc0d5d96c (patch) | |
| tree | d7a3a2029b037f51878d0d6256d9436c854af841 /src/Core/Thinning.idr | |
| parent | fe1f03b7cd7cfeb9992a968b5a5cbebe8fbe9b7d (diff) | |
Define weakening.
Diffstat (limited to 'src/Core/Thinning.idr')
| -rw-r--r-- | src/Core/Thinning.idr | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr index 0067ac4..dc4efcb 100644 --- a/src/Core/Thinning.idr +++ b/src/Core/Thinning.idr @@ -1,5 +1,7 @@ module Core.Thinning +import Data.Fin + -- Definition ------------------------------------------------------------------ data Thinner : Nat -> Nat -> Type where @@ -53,3 +55,16 @@ view IsId = Id m view (IsThinner IsBase) = Drop (id _) view (IsThinner (IsDrop thin)) = Drop (IsThinner thin) view (IsThinner (IsKeep thin)) = Keep (IsThinner thin) + +-- Weakening ------------------------------------------------------------------- + +wkn' : Fin m -> Thinner m n -> Fin n +wkn' i IsBase = FS i +wkn' i (IsDrop thin) = FS (wkn' i thin) +wkn' FZ (IsKeep thin) = FZ +wkn' (FS i) (IsKeep thin) = FS (wkn' i thin) + +export +wkn : Fin m -> m `Thins` n -> Fin n +wkn i IsId = i +wkn i (IsThinner thin) = wkn' i thin |