diff options
author | 2016-09-18 17:48:19 -0400 | |
---|---|---|
committer | 2016-09-18 17:48:19 -0400 | |
commit | 5b8d84cc0780929ef0fe3d4769c347b7d930549c (patch) | |
tree | 1445064df0ea2446c69a88f5fcb00415ce078099 | |
parent | 138b77db59ac11eb59fd63a28181dbc83445d173 (diff) |
Generalize SmartVarVar
-rw-r--r-- | src/Reflection/Syntax.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 061bb5d8c..e0defb9b4 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -127,10 +127,13 @@ Section language. [flat_type], and not just [base_type_code] *) Definition SmartVar {t} : interp_flat_type_gen var t -> exprf t := @smart_interp_flat_map var exprf (fun t => Var) (fun A B x y => Pair x y) t. + Definition SmartVarMap {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 SmartVarVar {t} : interp_flat_type_gen var t -> interp_flat_type_gen exprf t - := @smart_interp_flat_map var (interp_flat_type_gen exprf) (fun t => Var) (fun A B x y => pair x y) t. + := SmartVarMap (fun t => Var). Definition SmartConst {t} : interp_flat_type t -> interp_flat_type_gen exprf t - := @smart_interp_flat_map _ (interp_flat_type_gen exprf) (fun t => Const) (fun A B x y => pair x y) t. + := SmartVarMap (fun t => Const (t:=t)). End expr. Definition Expr (t : type) := forall var, @expr var t. |