add Var.tighten*

src/Quox/Syntax/Var.idr

@@ -263,3 +263,24 @@ decEqFromBool i j =
 %transform "Var.decEq" varDecEq = decEqFromBool
 
 public export %inline DecEq (Var n) where decEq = varDecEq
+
+parameters {auto _ : Alternative f}
+  export
+  tighten : OPE m n -> Var n -> f (Var m)
+  tighten Id       i      = pure i
+  tighten (Drop q) VZ     = empty
+  tighten (Drop q) (VS i) = tighten q i
+  tighten (Keep q) VZ     = pure VZ
+  tighten (Keep q) (VS i) = VS <$> tighten q i
+
+  export
+  tightenInner : {n : Nat} -> m `LTE` n -> Var n -> f (Var m)
+  tightenInner = tighten . dropInner
+
+  export
+  tightenN : (m : Nat) -> Var (m + n) -> f (Var n)
+  tightenN m = tighten $ dropInnerN m
+
+  export
+  tighten1 : Var (S n) -> f (Var n)
+  tighten1 = tightenN 1