diff options
Diffstat (limited to 'src/Experiments/NewPipeline/RewriterWf1.v')
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterWf1.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index 6ec85700a..d91ec0e69 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -1327,6 +1327,26 @@ Module Compilers. then UnderLets.interp ident_interp else (fun x => x)). + Fixpoint value'_interp_related1 + {with_lets1 t} + : @value' var with_lets1 t + -> var t + -> Prop + := match t return value' _ t -> var t -> Prop with + | type.base t + => fun v1 v2 + => expr.interp ident_interp (UnderLets_maybe_interp with_lets1 v1) + == v2 + | type.arrow s d + => fun (f1 : value' _ s -> value' _ d) (f2 : var s -> var d) + => forall x1 x2, + @value'_interp_related1 _ s x1 x2 + -> @value'_interp_related1 _ d (f1 x1) (f2 x2) + end. + + Definition value_interp_related1 {t} : @value var t -> var t -> Prop + := value'_interp_related1. + Fixpoint value'_interp_related {with_lets1 with_lets2 t} : @value' var with_lets1 t |