From fe7e75f74cc3b18f87c13b2aeadaf24f12f0001b Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 7 Jan 2017 21:10:17 -0500
Subject: Add apply10

---
 src/Util/Tower.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'src/Util/Tower.v')

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.
-- 
cgit v1.2.3