From 4d3d21d604243bc63774f4931f2313e20cdaf515 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 7 Jan 2017 21:18:51 -0500 Subject: Revert "Add apply10" This reverts commit fe7e75f74cc3b18f87c13b2aeadaf24f12f0001b. Revert "copy_bounds" This reverts commit 4c395e83de3c0baf7f8639fa2fbe2b62ba509682. Revert "Add Common10_4Op" This reverts commit 677733838139ff09d4a2dd9ff82258492a9a5bab. Revert "Add Expr10_4Op" This reverts commit 540740e8a423d0ec9d1dddb173f772c441dc0a1a. Revert "Add i10top_correct_and_bounded" This reverts commit bc4184ce6086971799630a0419881c8d344811ca. Revert "Add appify10" This reverts commit 66b63b406d9c78a0cecbbf89e5baf282231215c5. --- src/Util/Tower.v | 17 ----------------- 1 file changed, 17 deletions(-) (limited to 'src/Util/Tower.v') diff --git a/src/Util/Tower.v b/src/Util/Tower.v index f2709ef75..7f6bca59d 100644 --- a/src/Util/Tower.v +++ b/src/Util/Tower.v @@ -55,20 +55,3 @@ 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