From 8962d85902089a657aa06a39e50355c7c4c787da Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 2 Dec 2016 15:55:46 -0500 Subject: Add SmartFlatTypeMap --- src/Reflection/Syntax.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/Reflection/Syntax.v') diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 86e9b7002..cd20c78a0 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -290,6 +290,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 (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 (fun _ _ => Prod) t. Definition SmartVarMap {var var'} (f : forall t, var t -> var' t) (f' : forall t, var' t -> var t) {t} : interp_type_gen (interp_flat_type_gen var) t -> interp_type_gen (interp_flat_type_gen var') t := @smart_interp_map var (interp_type_gen (interp_flat_type_gen var')) f f' (fun A B x y => pair x y) (fun A B f x => f x) t. -- cgit v1.2.3