diff options
Diffstat (limited to 'src/Experiments/NewPipeline/RewriterWf1.v')
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterWf1.v | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index 0cbaaaacf..06c71e480 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -623,12 +623,11 @@ Module Compilers. | true, true => UnderLets.wf (fun G' v1 v2 - => exists (pf1 : anyexpr_ty v1 = t) (pf2 : anyexpr_ty v2 = t), - forall G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> wf_value G' v1' v2') - -> expr.wf G'' - (rew [fun t : base.type => expr t] pf1 in unwrap v1) - (rew [fun t : base.type => expr t] pf2 in unwrap v2)) + => exists (pf1 : anyexpr_ty v1 = t) (pf2 : anyexpr_ty v2 = t) G'', + (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> wf_value G' v1' v2') + /\ expr.wf G'' + (rew [fun t : base.type => expr t] pf1 in unwrap v1) + (rew [fun t : base.type => expr t] pf2 in unwrap v2)) G | false, false => UnderLets.wf (fun G' => wf_anyexpr G' t) G |