From 099bf0ceb14d85ab9c8862b615a349ac6a5b4aa4 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 31 Mar 2023 17:53:08 +0100
Subject: Define Var weakening.

---
 src/Core/Var.idr | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'src')

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)
-- 
cgit v1.2.3