diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-07 21:10:17 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-07 21:10:17 -0500 |
| commit | fe7e75f74cc3b18f87c13b2aeadaf24f12f0001b (patch) | |
| tree | 93f9757b05b64341d0415a74d3f15e02486caec7 /src/Util/Tower.v | |
| parent | 4c395e83de3c0baf7f8639fa2fbe2b62ba509682 (diff) | |
Add apply10
Diffstat (limited to 'src/Util/Tower.v')
| -rw-r--r-- | src/Util/Tower.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/Util/Tower.v b/src/Util/Tower.v index 7f6bca59d..f2709ef75 100644 --- a/src/Util/Tower.v +++ b/src/Util/Tower.v @@ -55,3 +55,20 @@ Definition apply9_nd {BK PA PB ARR} : PB (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR B))))))))) := @apply9 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F) tt tt tt tt tt tt tt tt tt B f. + +Definition apply10 {AK BK PA PB ARR} + (F : forall (A : AK) (B : BK), (PA A -> PB B) -> PB (ARR A B)) + {A0 A1 A2 A3 A4 A5 A6 A7 A8 A9 : AK} {B : BK} + (f : PA A0 -> PA A1 -> PA A2 -> PA A3 -> PA A4 -> PA A5 -> PA A6 -> PA A7 -> PA A8 -> PA A9 -> PB B) + : PB (ARR A0 (ARR A1 (ARR A2 (ARR A3 (ARR A4 (ARR A5 (ARR A6 (ARR A7 (ARR A8 (ARR A9 B)))))))))). +Proof. + repeat (apply F; intro); apply f; assumption. +Defined. + +Definition apply10_nd {BK PA PB ARR} + (F : forall (B : BK), (PA -> PB B) -> PB (ARR B)) + {B : BK} + (f : tower_nd PA (PB B) 10) + : PB (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR B)))))))))) + := @apply10 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F) + tt tt tt tt tt tt tt tt tt tt B f. |