diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-09 15:31:30 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-09 15:31:39 -0500 |
commit | 9a347ce6e39cc98af22a9eb76f2801935befdd8e (patch) | |
tree | b4ff8fe1bb6bb64249618fe996b39a5856e02641 /src/Reflection/Syntax.v | |
parent | ba1c1c48eaf8b635805f47e60c56768e44a2c4c7 (diff) |
Add Syntax.tuple_map
Diffstat (limited to 'src/Reflection/Syntax.v')
-rw-r--r-- | src/Reflection/Syntax.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 98845ca27..3f1fec3c7 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -179,6 +179,13 @@ Section language. Lemma flat_interp_tuple_untuple' {T n v} : @flat_interp_tuple T (S n) (flat_interp_untuple' v) = v. Proof. apply flat_interp_tuple'_untuple'. Qed. + Definition tuple_map {A B n} (f : interp_flat_type A -> interp_flat_type B) (v : interp_flat_type (tuple A n)) + : interp_flat_type (tuple B n) + := let fv := Tuple.map f (flat_interp_tuple v) in + match n return interp_flat_type (tuple A n) -> Tuple.tuple (interp_flat_type B) n -> interp_flat_type (tuple B n) with + | 0 => fun v _ => f v + | S _ => fun v fv => flat_interp_untuple' fv + end v fv. Section rel. Context (R : forall t, interp_base_type t -> interp_base_type t -> Prop). Fixpoint interp_flat_type_rel_pointwise (t : flat_type) |