diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-24 15:52:23 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-24 15:52:23 -0500 |
| commit | a962b7faf9991a8890e1a117ab478272e4390f8d (patch) | |
| tree | 2b7d6a4a561a13b9df568b46056944bd02760e5e /src/Reflection/Syntax.v | |
| parent | 525032e2662840e3c11dec5179467e09109a0cac (diff) | |
Add SmartVarfMap2
Diffstat (limited to 'src/Reflection/Syntax.v')
| -rw-r--r-- | src/Reflection/Syntax.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 46a91e30b..fc8e5004e 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -187,6 +187,9 @@ Section language. Definition SmartVarfMap {var var'} (f : forall t, var t -> var' t) {t} : interp_flat_type_gen var t -> interp_flat_type_gen var' t := @smart_interp_flat_map var (interp_flat_type_gen var') f tt (fun A B x y => pair x y) t. + Definition SmartVarfMap2 {var var' var''} (f : forall t, var t -> var' t -> var'' t) {t} + : interp_flat_type_gen var t -> interp_flat_type_gen var' t -> interp_flat_type_gen var'' t + := @smart_interp_flat_map2 var var' (interp_flat_type_gen var'') f tt (fun A B x y => pair x y) t. Definition SmartFlatTypeMap {var'} (f : forall t, var' t -> base_type_code) {t} : interp_flat_type_gen var' t -> flat_type := @smart_interp_flat_map var' (fun _ => flat_type) f Unit (fun _ _ => Prod) t. @@ -330,6 +333,7 @@ Global Arguments SmartPairf {_ _ _ t} _. Global Arguments SmartValf {_} T _ t. Global Arguments SmartVarVarf {_ _ _ _} _. Global Arguments SmartVarfMap {_ _ _} _ {_} _. +Global Arguments SmartVarfMap2 {_ _ _ _} _ {t} _ _. Global Arguments SmartFlatTypeMap {_ _} _ {_} _. Global Arguments SmartFlatTypeMapInterp {_ _ _ _} _ {_} _. Global Arguments SmartFlatTypeMapUnInterp {_ _ _ _ _} fv {_ _} _. |