From fba865c2784d376f34dec543087d29db3d5090b7 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Fri, 31 Mar 2023 18:14:53 +0100 Subject: Define Env indexing. --- src/Core/Term/Environment.idr | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'src/Core') diff --git a/src/Core/Term/Environment.idr b/src/Core/Term/Environment.idr index 8e7ce4f..1cc7ba8 100644 --- a/src/Core/Term/Environment.idr +++ b/src/Core/Term/Environment.idr @@ -2,6 +2,8 @@ module Core.Term.Environment import Core.Context import Core.Term +import Core.Thinning +import Core.Var -- Definition ------------------------------------------------------------------ @@ -11,3 +13,23 @@ data Env : Context -> Type where (:<) : Env sx -> Term sx -> Env (sx :< n) %name Env env + +-- Operations ------------------------------------------------------------------ + +record IndexResult (sx : Context) where + constructor MkRes + {0 sy : Context} + val : Term sy + 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) = + let MkRes val thin = doIndex env $ view i in + MkRes val (drop thin _) + +export +index : Env sx -> Var sx -> Term sx +index env i = + let MkRes val thin = doIndex env $ view i in + wkn val thin -- cgit v1.2.3