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 | |
| parent | fe1f03b7cd7cfeb9992a968b5a5cbebe8fbe9b7d (diff) | |
Define weakening.
Diffstat (limited to 'src')
| -rw-r--r-- | src/Core/Term.idr | 12 | ||||
| -rw-r--r-- | src/Core/Thinning.idr | 15 |
2 files changed, 27 insertions, 0 deletions
diff --git a/src/Core/Term.idr b/src/Core/Term.idr index 7fea482..1b050ca 100644 --- a/src/Core/Term.idr +++ b/src/Core/Term.idr @@ -1,5 +1,7 @@ module Core.Term +import Core.Thinning + import public Data.Fin -- Definition ------------------------------------------------------------------ @@ -15,3 +17,13 @@ data Term : Nat -> Type where App : Term n -> Term n -> Term n %name Term t, u, v + +-- Weakening ------------------------------------------------------------------- + +public export +wkn : Term m -> m `Thins` n -> Term n +wkn (Var i) thin = Var (wkn i thin) +wkn Set thin = Set +wkn (Pi t u) thin = Pi (wkn t thin) (wkn u $ keep thin) +wkn (Abs t) thin = Abs (wkn t $ keep thin) +wkn (App t u) thin = App (wkn t thin) (wkn u thin) 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 |