From c7321e0061137232f38598378c2d0c380f872082 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Mar 2022 17:18:36 -0700 Subject: [PATCH] chore: remove revert hack from example --- tests/lean/run/constProp.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/tests/lean/run/constProp.lean b/tests/lean/run/constProp.lean index 22cca448ad..dcc5e86471 100644 --- a/tests/lean/run/constProp.lean +++ b/tests/lean/run/constProp.lean @@ -347,10 +347,9 @@ theorem Stmt.simplify_correct (h : (σ, s) ⇓ σ') : (σ, s.simplify) ⇓ σ' : | assign => apply Bigstep.assign; simp [*] | whileTrue heq h₁ h₂ ih₁ ih₂ => rw [← Expr.eval_simplify] at heq - revert ih₂ -- This is a hack to make sure the next split simplify the two match expressions: TODO: make sure `simp` can do it - split <;> intro ih₂ + split next h => rw [h] at heq; simp at heq - next => apply Bigstep.whileTrue heq ih₁ ih₂ + next hnp => simp [hnp] at ih₂; apply Bigstep.whileTrue heq ih₁ ih₂ | whileFalse heq => split next => exact Bigstep.skip