Pass around an accumMap (but it's empty still)

1 files changed, 9 insertions, 0 deletions

diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs
index dbb37f7..bd2c244 100644
--- a/src/AST/Weaken.hs
+++ b/src/AST/Weaken.hs
@@ -36,6 +36,15 @@ splitIdx SNil i = Right i
 splitIdx (SCons _ _) IZ = Left IZ
 splitIdx (SCons _ l) (IS i) = first IS (splitIdx l i)
 
+slistIdx :: SList f list -> Idx list t -> f t
+slistIdx (SCons x _) IZ = x
+slistIdx (SCons _ list) (IS i) = slistIdx list i
+slistIdx SNil i = case i of {}
+
+idx2int :: Idx env t -> Int
+idx2int IZ = 0
+idx2int (IS n) = 1 + idx2int n
+
 data env :> env' where
   WId :: env :> env
   WSink :: forall t env. env :> (t : env)