diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-22 19:09:15 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-22 23:34:24 -0500 |
commit | a63973a4e9388a66575c64057e389995e341426d (patch) | |
tree | d7c627d04eabadc4ca59581338efad6c93f728f2 /src/Util | |
parent | 9f0102d8c0c2a35cb14d7ebf9020b74ea4bcccbe (diff) |
Add impl_under_tower
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Tower.v | 25 |
1 files changed, 19 insertions, 6 deletions
diff --git a/src/Util/Tower.v b/src/Util/Tower.v index 20d737b96..7f6bca59d 100644 --- a/src/Util/Tower.v +++ b/src/Util/Tower.v @@ -1,12 +1,25 @@ 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. + Context (A : Type). + Section with_B. + Context (B : Type). + Fixpoint tower_nd (n : nat) + := match n with + | 0 => B + | S n' => A -> tower_nd n' + end. + End with_B. + + Section with_B2. + Context (B B' : Type) (f : B -> B'). + Fixpoint impl_under_tower_nd (n : nat) + : tower_nd B n -> tower_nd B' n + := match n with + | 0 => f + | S n' => fun t x => impl_under_tower_nd n' (t x) + end. + End with_B2. End tower_nd. Definition apply4 {AK BK PA PB ARR} |