diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-22 17:02:40 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-22 23:31:34 -0500 |
| commit | e01bc703cfcb2aa0a0a5c3bdfe6696cefdfb8215 (patch) | |
| tree | 1dce0c9fd07ff44d3d266b0f178c03a254019a0f /src/Util/Tower.v | |
| parent | a84ea5b4efff70f4037ba480508ffcc069a6a96d (diff) | |
Add tower_nd
Diffstat (limited to 'src/Util/Tower.v')
| -rw-r--r-- | src/Util/Tower.v | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/Util/Tower.v b/src/Util/Tower.v index e3f57f3ed..20d737b96 100644 --- a/src/Util/Tower.v +++ b/src/Util/Tower.v @@ -1,5 +1,14 @@ Require Export Crypto.Util.FixCoqMistakes. +Section tower_nd. + Context (A : Type) (B : Type). + Fixpoint tower_nd (n : nat) + := match n with + | 0 => B + | S n' => A -> tower_nd n' + end. +End tower_nd. + Definition apply4 {AK BK PA PB ARR} (F : forall (A : AK) (B : BK), (PA A -> PB B) -> PB (ARR A B)) {A0 A1 A2 A3 : AK} {B : BK} @@ -12,7 +21,7 @@ Defined. Definition apply4_nd {BK PA PB ARR} (F : forall (B : BK), (PA -> PB B) -> PB (ARR B)) {B : BK} - (f : PA -> PA -> PA -> PA -> PB B) + (f : tower_nd PA (PB B) 4) : PB (ARR (ARR (ARR (ARR B)))) := @apply4 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F) tt tt tt tt B f. @@ -29,7 +38,7 @@ Defined. Definition apply9_nd {BK PA PB ARR} (F : forall (B : BK), (PA -> PB B) -> PB (ARR B)) {B : BK} - (f : PA -> PA -> PA -> PA -> PA -> PA -> PA -> PA -> PA -> PB B) + (f : tower_nd PA (PB B) 9) : 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. |