local の追加漏れ修正

lean-ja · Oct 13, 2024 · 9c64b2e · 9c64b2e
1 parent 32ceb38
commit 9c64b2e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/LeanByExample/Reference/Declarative/AddAesopRules.lean b/LeanByExample/Reference/Declarative/AddAesopRules.lean
@@ -224,7 +224,7 @@ example (a b : Nat) (h : 3 ∣ (10 * a + b)) : 3 ∣ (a + b) := by
   omega
 
 -- aesop にルールを登録する
-add_aesop_rules safe tactic [(by omega)]
+local add_aesop_rules safe tactic [(by omega)]
 
 example (a b : Nat) (h : 3 ∣ (10 * a + b)) : 3 ∣ (a + b) := by
   -- aesop で証明できるようになった!