blob: 4f167f9fa890485fad1801324a88ca7485e252ea (
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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
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
-- Equality --------------------------------------------------------------------
namespace Eq
public export
data EnvEq : Env sx -> Env sx -> Type where
Lin : EnvEq [<] [<]
Add :
EnvEq env1 env2 ->
Term.wkn t thin1 = wkn u thin2 ->
EnvEq (Add env1 thin1 t) (Add env2 thin2 u)
%name EnvEq prf
public export
(:<) : EnvEq env1 env2 -> (0 t : Term sx) -> EnvEq (env1 :< t) (env2 :< t)
prf :< t = Add prf Refl
|
