diff options
Diffstat (limited to 'src/UnderLets.v')
-rw-r--r-- | src/UnderLets.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/UnderLets.v b/src/UnderLets.v index 34cecf322..6a484cf7d 100644 --- a/src/UnderLets.v +++ b/src/UnderLets.v @@ -137,6 +137,22 @@ Module Compilers. Notation "x <----- y ; f" := (UnderLets.splice_option y (fun x => f%under_lets)) : under_lets_scope. End Notations. + Section with_var2. + Context {base_type : Type}. + Local Notation type := (type base_type). + Context {ident1 var1 ident2 var2 : type -> Type} + (f : forall t, @expr base_type ident1 var1 t -> @expr base_type ident2 var2 t) + (f' : forall t, var2 t -> var1 t) + {T : Type}. + + Fixpoint map (x : @UnderLets base_type ident1 var1 T) : @UnderLets base_type ident2 var2 T + := match x with + | UnderLet A x F + => UnderLet (f A x) (fun v => map (F (f' A v))) + | Base x => Base x + end. + End with_var2. + Section reify. Context {var : type.type base.type -> Type}. Local Notation type := (type.type base.type). |