blob: dc4efcbc70f4bf4e50a99f8bef93d550815b845b (
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
61
62
63
64
65
66
67
68
69
70
|
module Core.Thinning
import Data.Fin
-- Definition ------------------------------------------------------------------
data Thinner : Nat -> Nat -> Type where
IsBase : Thinner n (S n)
IsDrop : Thinner m n -> Thinner m (S n)
IsKeep : Thinner m n -> Thinner (S m) (S n)
export
data Thins : Nat -> Nat -> Type where
IsId : n `Thins` n
IsThinner : Thinner m n -> m `Thins` n
%name Thinner thin
%name Thins thin
-- Constructors ----------------------------------------------------------------
export
id : (0 n : Nat) -> n `Thins` n
id n = IsId
export
drop : m `Thins` n -> m `Thins` S n
drop IsId = IsThinner IsBase
drop (IsThinner thin) = IsThinner (IsDrop thin)
export
keep : m `Thins` n -> S m `Thins` S n
keep IsId = IsId
keep (IsThinner thin) = IsThinner (IsKeep thin)
-- Non-Identity ----------------------------------------------------------------
export
data IsNotId : m `Thins` n -> Type where
ItIsThinner : IsNotId (IsThinner thin)
%name IsNotId prf
-- Views -----------------------------------------------------------------------
public export
data View : m `Thins` n -> Type where
Id : (0 n : Nat) -> View (id n)
Drop : (thin : m `Thins` n) -> View (drop thin)
Keep : (thin : m `Thins` n) -> {auto 0 prf : IsNotId thin} -> View (keep thin)
export
view : (thin : m `Thins` n) -> View thin
view IsId = Id m
view (IsThinner IsBase) = Drop (id _)
view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)
-- Weakening -------------------------------------------------------------------
wkn' : Fin m -> Thinner m n -> Fin n
wkn' i IsBase = FS i
wkn' i (IsDrop thin) = FS (wkn' i thin)
wkn' FZ (IsKeep thin) = FZ
wkn' (FS i) (IsKeep thin) = FS (wkn' i thin)
export
wkn : Fin m -> m `Thins` n -> Fin n
wkn i IsId = i
wkn i (IsThinner thin) = wkn' i thin
|
