blob: 340afffc914bc2fb85c6cd8cb0731e91b504f5b6 (
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 Obs.Substitution
import Data.Fin
%default total
public export
interface Rename (0 x : Nat -> Type) where
rename : forall m, n . x n -> (Fin n -> Fin m) -> x m
public export
interface Rename x => PointedRename x where
point : forall n . Fin n -> x n
public export
interface Subst (0 x, y, z : Nat -> Type) where
subst : forall m, n . x n -> (Fin n -> y m) -> z m
public export
Rename x => Subst x Fin x where
subst = rename
public export
Rename Fin where
rename i f = f i
public export
PointedRename Fin where
point = id
public export
add : (0 x : _) -> x n -> (Fin m -> x n) -> Fin (S m) -> x n
add x v f FZ = v
add x v f (FS i) = f i
public export
lift : PointedRename x => (k : _) -> (Fin m -> x n) -> Fin (k + m) -> x (k + n)
lift 0 f = f
lift (S k) f = add x (point FZ) (\i => rename (lift k f i) FS)
public export
weaken : Rename x => (m : _) -> x n -> x (m + n)
weaken m t = rename t (shift m)
|
