Merge pull request #1272 from lean-ja/Seasawher/issue1268

複数ファイルからなる記事の扱いについて

Author: Seasawher

LeanByExample/Declarative/DeclareAesopRuleSets.lean

@@ -9,16 +9,12 @@
 ## 基本的な使い方
 
 `declare_aesop_rule_sets` で宣言されたルールセットは、宣言したそのファイルの中では有効になりません。`import` する必要があります。前提として以下の内容のファイルを `import` しているとしましょう。
-```lean
-/- import されているファイルの内容 -/
-import Aesop
 
-declare_aesop_rule_sets [HogeRules]
-```
+{{#include ./DeclareAesopRuleSetsLib.md}}
 
 このとき、以下のように `aesop` の `rule_sets` に `HogeRules` を渡すことで、`HogeRules` に登録されたルールセットを使用することができます。
 -/
-import LeanByExample.Declarative.DeclareAesopRuleSetsLib --#
+import LeanByExample.Declarative.DeclareAesopRuleSetsLib -- インポートで有効になる
 import Mathlib.Tactic.Says --#
 
 example : True := by

LeanByExample/Declarative/DeclareAesopRuleSetsLib.lean

@@ -1,3 +1,4 @@
+-- import されているファイルの内容
 import Aesop
 
 declare_aesop_rule_sets [HogeRules]