|
adam@6
|
1 (** A constructor equality predicate *)
|
|
adam@6
|
2
|
|
adam@6
|
3 con eq :: K --> K -> K -> Type
|
|
adam@6
|
4
|
|
adam@6
|
5 val refl : K --> t ::: K -> eq t t
|
|
adam@6
|
6 val sym : K --> t1 ::: K -> t2 ::: K -> eq t1 t2 -> eq t2 t1
|
|
adam@6
|
7 val trans : K --> t1 ::: K -> t2 ::: K -> t3 ::: K -> eq t1 t2 -> eq t2 t3 -> eq t1 t3
|
|
adam@6
|
8
|
|
adam@6
|
9 val cast : K --> t1 ::: K -> t2 ::: K -> eq t1 t2 -> f :: (K -> Type) -> f t1 -> f t2
|
|
adam@6
|
10
|
|
adam@6
|
11 val fold : K --> tf :: ({K} -> Type) -> r ::: {K}
|
|
adam@6
|
12 -> (pre :: {K} -> nm :: Name -> v :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
|
|
adam@6
|
13 eq r (pre ++ [nm = v] ++ post) -> tf post -> tf ([nm = v] ++ post))
|
|
adam@6
|
14 -> tf [] -> folder r -> tf r
|
|
adam@6
|
15
|
|
adam@6
|
16 val foldUR : tr :: Type -> tf :: ({Unit} -> Type) -> r ::: {Unit}
|
|
adam@6
|
17 -> (pre :: {Unit} -> nm :: Name -> post :: {Unit} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
|
|
adam@6
|
18 eq r (pre ++ [nm] ++ post) -> tr -> tf post -> tf ([nm] ++ post))
|
|
adam@6
|
19 -> tf [] -> folder r -> $(mapU tr r) -> tf r
|
|
adam@6
|
20
|
|
adam@6
|
21 val foldR : K --> tr :: (K -> Type) -> tf :: ({K} -> Type) -> r ::: {K}
|
|
adam@6
|
22 -> (pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
|
|
adam@6
|
23 eq r (pre ++ [nm = t] ++ post) -> tr t -> tf post -> tf ([nm = t] ++ post))
|
|
adam@6
|
24 -> tf [] -> folder r -> $(map tr r) -> tf r
|
|
adam@6
|
25
|
|
adam@6
|
26 val foldR2 : K --> tr1 :: (K -> Type) -> tr2 :: (K -> Type) -> tf :: ({K} -> Type) -> r ::: {K}
|
|
adam@6
|
27 -> (pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
|
|
adam@6
|
28 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tf post -> tf ([nm = t] ++ post))
|
|
adam@6
|
29 -> tf [] -> folder r -> $(map tr1 r) -> $(map tr2 r) -> tf r
|
|
adam@6
|
30
|
|
adam@6
|
31 val foldR3 : K --> tr1 :: (K -> Type) -> tr2 :: (K -> Type) -> tr3 :: (K -> Type) -> tf :: ({K} -> Type) -> r ::: {K}
|
|
adam@6
|
32 -> (pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
|
|
adam@6
|
33 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tf post -> tf ([nm = t] ++ post))
|
|
adam@6
|
34 -> tf [] -> folder r -> $(map tr1 r) -> $(map tr2 r) -> $(map tr3 r) -> tf r
|
|
adam@6
|
35
|
|
adam@6
|
36 val foldR4 : K --> tr1 :: (K -> Type) -> tr2 :: (K -> Type) -> tr3 :: (K -> Type) -> tr4 :: (K -> Type) -> tf :: ({K} -> Type) -> r ::: {K}
|
|
adam@6
|
37 -> (pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
|
|
adam@6
|
38 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tr4 t -> tf post -> tf ([nm = t] ++ post))
|
|
adam@6
|
39 -> tf [] -> folder r -> $(map tr1 r) -> $(map tr2 r) -> $(map tr3 r) -> $(map tr4 r) -> tf r
|
|
adam@6
|
40
|
|
adam@6
|
41 val mp : K --> tr :: (K -> Type) -> tf :: (K -> Type) -> r ::: {K}
|
|
adam@6
|
42 -> (nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] =>
|
|
adam@6
|
43 eq r ([nm = t] ++ rest) -> tr t -> tf t)
|
|
adam@6
|
44 -> folder r -> $(map tr r) -> $(map tf r)
|
