From 61911f8a41a264c9066f9e145597157b3ebf6a79 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 27 Feb 2019 17:11:03 -0500 Subject: Add UnderLets.map --- src/UnderLets.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'src/UnderLets.v') 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). -- cgit v1.2.3