diff options
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 |