diff --git a/LeanByExample/Declarative/AddAesopRules.lean b/LeanByExample/Declarative/AddAesopRules.lean index 7d7e152c..af82b043 100644 --- a/LeanByExample/Declarative/AddAesopRules.lean +++ b/LeanByExample/Declarative/AddAesopRules.lean @@ -22,7 +22,7 @@ example : Pos 1 := by aesop /- なお `aesop` をカスタマイズしたものを専用のタクティクにまとめることも可能ですが、それについてはここでは詳しく述べません。[`declare_aesop_rule_sets`](#{root}/Declarative/DeclareAesopRuleSets.md) コマンドのページを参照してください。 -`add_aesop_rules` は、`add_aesop_rules ? ? ? ?]` という構文で使用できます。 +`add_aesop_rules` は、`add_aesop_rules ? ? ? ?` という構文で使用できます。 ## phase について