blob: 62e3b602f1b219c829f1f825babcd661c54a04e2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
module Core.Term.Environment
import Core.Context
import Core.Term
import Core.Thinning
import Core.Var
%prefix_record_projections off
-- Definition ------------------------------------------------------------------
public export
data Env : Context -> Type where
Lin : Env [<]
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
constructor MkRes
{0 sy : Context}
val : Term sy
thin : sy `Thins` sx
doIndex : Env sx -> {0 i : Var sx} -> View i -> IndexResult sx
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 _)
export
index : Env sx -> Var sx -> Term sx
index env i =
let MkRes val thin = doIndex env $ view i in
wkn val thin
|
