Make environments do weakening lazily.

This is in anticipation for defining well-formed thinnings.

1 files changed, 9 insertions, 3 deletions

diff --git a/src/Core/Term/Environment.idr b/src/Core/Term/Environment.idr
index 7b05ec0..62e3b60 100644
--- a/src/Core/Term/Environment.idr
+++ b/src/Core/Term/Environment.idr
@@ -12,10 +12,16 @@ import Core.Var
 public export
 data Env : Context -> Type where
   Lin : Env [<]
-  (:<) : Env sx -> Term sx -> Env (sx :< n)
+  Add : Env sx -> sy `Thins` sx -> Term sy -> Env (sx :< n)
 
 %name Env env
 
+-- Constructors ----------------------------------------------------------------
+
+public export
+(:<) : Env sx -> Term sx -> Env (sx :< n)
+env :< t = Add env (id _) t
+
 -- Operations ------------------------------------------------------------------
 
 record IndexResult (sx : Context) where
@@ -25,8 +31,8 @@ record IndexResult (sx : Context) where
   thin : sy `Thins` sx
 
 doIndex : Env sx -> {0 i : Var sx} -> View i -> IndexResult sx
-doIndex (env :< t) Here = MkRes t (drop (id _) _)
-doIndex (env :< t) (There i) =
+doIndex (Add env thin t) Here = MkRes t (drop thin _)
+doIndex (Add env thin t) (There i) =
   let MkRes val thin = doIndex env $ view i in
   MkRes val (drop thin _)