Define Var weakening.

1 files changed, 13 insertions, 0 deletions

diff --git a/src/Core/Var.idr b/src/Core/Var.idr
index 25648e5..29c6476 100644
--- a/src/Core/Var.idr
+++ b/src/Core/Var.idr
@@ -1,6 +1,7 @@
 module Core.Var
 
 import Core.Context
+import Core.Thinning
 
 -- Variables -------------------------------------------------------------------
 
@@ -41,3 +42,15 @@ export
 view : (i : Var sx) -> View i
 view (MakeVar 0 Here) = Here
 view (MakeVar (S k) (There prf)) = There (MakeVar k prf)
+
+-- Operations ------------------------------------------------------------------
+
+doWkn : Var sx -> {0 thin : sx `Thins` sy} -> View thin -> Var sy
+doWkn i (Id sy) = i
+doWkn i (Drop thin n) = there $ doWkn i (view thin)
+doWkn (MakeVar 0 Here) (Keep thin n _) = here
+doWkn (MakeVar (S k) (There prf)) (Keep thin n _) = there $ doWkn (MakeVar k prf) (view thin)
+
+export
+wkn : Var sx -> sx `Thins` sy -> Var sy
+wkn i thin = doWkn i (view thin)