修正

Seasawher · Sep 15, 2024 · 583a1e9 · 583a1e9
1 parent 13cd193
commit 583a1e9
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/ConcreteSemantics/Equivalence.lean b/ConcreteSemantics/Equivalence.lean
@@ -40,6 +40,7 @@ macro_rules
   | `(tactic|unfold ≈) => `(tactic| dsimp only [(· ≈ ·), Setoid.r, equivCmd])
 
 -- big_step が `unfold ≈` を利用できるようにする
+-- これでゴールに `≈` が含まれている場合に対応できる
 add_aesop_rules norm [tactic (by unfold ≈) (rule_sets := [BigStepRules])]
 
 /-- ### Lemma 7.3

diff --git a/ConcreteSemantics/RuleInversion.lean b/ConcreteSemantics/RuleInversion.lean
@@ -92,7 +92,7 @@ theorem while_iff {B S s u} : (whileDo B S, s) ==> u ↔
   big_step
 
 /-- while の条件式が真のときの inversion rule -/
-@[simp] theorem while_true_iff {B S s u} (hcond : B s) : (whileDo B S, s) ==> u ↔
+theorem while_true_iff {B S s u} (hcond : B s) : (whileDo B S, s) ==> u ↔
     (∃ t, (S, s) ==> t ∧ (whileDo B S, t) ==> u) := by
   big_step