blob: 9914697628bb0eb1b5159d8478927e3dbe64eb85 (
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
|
module Core.Environment.Extension
import Core.Environment
import Core.Term.Thinned
import Core.Thinning
-- Definition ------------------------------------------------------------------
public export
data Extends : m `Thins` n -> Env n -> Env m -> Type where
Id : Extends (id n) env env
Drop : Extends thin env1 env2 -> Extends (drop thin) (env1 :< a) env2
Keep : Extends thin env1 env2 -> Extends (keep thin) (env1 :< wkn a thin) (env2 :< a)
%name Extends ext
-- Composition -----------------------------------------------------------------
public export
(.) : Extends thin2 env3 env2 -> Extends thin1 env2 env1 -> Extends (thin2 . thin1) env3 env1
Id . ext1 =
rewrite compLeftId thin1 in
ext1
Drop {thin = thin2} ext2 . ext1 =
rewrite compLeftDrop thin2 thin1 in
Drop (ext2 . ext1)
Keep {thin = thin2} ext2 . Id =
rewrite compRightId (keep thin2) in
Keep ext2
Keep {thin = thin2} ext2 . Drop {thin = thin1} ext1 =
rewrite compRightDrop thin2 thin1 in
Drop (ext2 . ext1)
Keep {thin = thin2} ext2 . Keep {thin = thin1, a} ext1 =
rewrite compKeep thin2 thin1 in
rewrite wknHomo a thin1 thin2 in
Keep (ext2 . ext1)
|
