diff options
| -rw-r--r-- | src/Core/Declarative.idr | 4 | ||||
| -rw-r--r-- | src/Core/Term/Environment.idr | 12 |
2 files changed, 11 insertions, 5 deletions
diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr index 8efda89..4a27923 100644 --- a/src/Core/Declarative.idr +++ b/src/Core/Declarative.idr @@ -27,9 +27,9 @@ data EnvWf where EnvWf [<] (:<) : EnvWf env -> - TypeWf env a -> + TypeWf env (wkn a thin) -> --- - EnvWf (env :< a) + EnvWf (Add env thin a) data TypeWf where SetType : 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 _) |