From 6ce6cf4580f2c0ab4c7c4ec56f438c1cc184c7cd Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 12 Nov 2024 18:05:25 +0000
Subject: Add more names. Names are good.

---
 src/Inky/Term/Substitution.idr | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'src/Inky/Term/Substitution.idr')

diff --git a/src/Inky/Term/Substitution.idr b/src/Inky/Term/Substitution.idr
index 791014b..690e38c 100644
--- a/src/Inky/Term/Substitution.idr
+++ b/src/Inky/Term/Substitution.idr
@@ -110,24 +110,24 @@ thinTyBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ thinTyBranchesName
 
 public export
 Env : Mode -> Type -> SnocList String -> SnocList String -> SnocList String -> Type
-Env mode m tyCtx ctx1 ctx2 = All (const $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
+Env mode m tyCtx ctx1 ctx2 = All (Assoc0 $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
 
 public export
 Env' : Mode -> Type -> SnocList String -> List String -> SnocList String -> Type
-Env' mode m tyCtx ctx1 ctx2 = All (const $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
+Env' mode m tyCtx ctx1 ctx2 = All (Assoc0 $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
 
 public export
 thinEnv :
   ctx2 `Thins` ctx3 ->
   Env mode m tyCtx ctx1 ctx2 ->
   Env mode m tyCtx ctx1 ctx3
-thinEnv f = mapProperty (bimap (index f) (thin $ f))
+thinEnv f = mapProperty (map $ bimap (index f) (thin $ f))
 
 public export
 lift :
   Env mode m tyCtx ctx1 ctx2 ->
   Env mode m tyCtx (ctx1 :< x) (ctx2 :< x)
-lift f = thinEnv (Drop Id) f :< Left (%% x)
+lift f = thinEnv (Drop Id) f :< (x :- Left (%% x))
 
 public export
 sub :
@@ -160,12 +160,12 @@ keepBound :
   forall ctx. {0 bound : List String} ->
   LengthOf bound -> Env' mode m tyCtx bound (ctx <>< bound)
 keepBound Z = []
-keepBound (S len) = Left (index (dropFish Id len) (toVar Here)) :: keepBound len
+keepBound (S len) = (_ :- Left (index (dropFish Id len) (toVar Here))) :: keepBound len
 
 sub f (Annot meta t a) = Annot meta (sub f t) a
-sub f (Var meta i) = either (Var meta) id $ indexAll i.pos f
+sub f (Var meta i) = either (Var meta) id (indexAll i.pos f).value
 sub f (Let meta e (x ** t)) = Let meta (sub f e) (x ** sub (lift f) t)
-sub f (LetTy meta a (x ** t)) = LetTy meta a (x ** sub (mapProperty (map $ thinTy (Drop Id)) f) t)
+sub f (LetTy meta a (x ** t)) = LetTy meta a (x ** sub (mapProperty (map $ map $ thinTy (Drop Id)) f) t)
 sub f (Abs meta (bound ** t)) =
   let len = lengthOf bound in
   Abs meta (bound ** sub (thinEnv (dropFish Id len) f <>< keepBound len) t)
-- 
cgit v1.2.3