blob: 284a23057c3e1b3c82aa37c1499dbcf74cd0a08f (
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
|
module CC.Thinning
-- Definition ------------------------------------------------------------------
export
data Thins : (src, tgt : SnocList a) -> Type where
IsEmpty : [<] `Thins` [<]
IsDrop : src `Thins` tgt -> src `Thins` tgt :< x
IsKeep : src `Thins` tgt -> src :< x `Thins` tgt :< x
%name Thins thin
-- Operations ------------------------------------------------------------------
export
empty : [<] `Thins` [<]
empty = IsEmpty
export
drop : src `Thins` tgt -> src `Thins` tgt :< x
drop thin = IsDrop thin
export
keep : src `Thins` tgt -> src :< x `Thins` tgt :< x
keep thin = IsKeep thin
export
id : {ctx : SnocList a} -> ctx `Thins` ctx
id {ctx = [<]} = empty
id {ctx = _ :< _} = keep id
-- Views -----------------------------------------------------------------------
public export
data View : src `Thins` tgt -> Type where
Empty : View CC.Thinning.empty
Drop : (thin : src `Thins` tgt) -> View (drop thin)
Keep : (thin : src `Thins` tgt) -> View (keep thin)
%name View view
public export
view : (thin : src `Thins` tgt) -> View thin
view IsEmpty = Empty
view (IsDrop thin) = Drop thin
view (IsKeep thin) = Keep thin
|
