diff options
Diffstat (limited to 'src/Experiments/NewPipeline/RewriterRulesInterpGood.v')
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesInterpGood.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v index 2bad756c9..b205acec1 100644 --- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v @@ -345,6 +345,13 @@ Module Compilers. Proof using Type. Time start_interp_good. Time all: try solve [ repeat interp_good_t_step; (lia + nia) ]. + Qed. + + Lemma arith_with_casts_rewrite_rules_interp_good + : rewrite_rules_interp_goodT arith_with_casts_rewrite_rules. + Proof using Type. + Time start_interp_good. + Time all: try solve [ repeat interp_good_t_step; (lia + nia) ]. (* This is mainly for display *) all: repeat first [ progress cbn [Compile.value' Compile.reify] in * | progress subst @@ -459,13 +466,6 @@ subgoal 9 (ID 33473) is: 1-9: exact admit. Qed. - Lemma arith_with_casts_rewrite_rules_interp_good - : rewrite_rules_interp_goodT arith_with_casts_rewrite_rules. - Proof using Type. - Time start_interp_good. - Time all: try solve [ repeat interp_good_t_step; (lia + nia) ]. - Qed. - Local Ltac fancy_local_t := repeat first [ match goal with | [ H : forall s v v', ?invert_low s v = Some v' -> v = _, |