diff options
Diffstat (limited to 'src/Core/Term')
| -rw-r--r-- | src/Core/Term/Environment.idr | 12 |
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 _) |