diff --git a/LeanByExample/Declarative/DeclareAesopRuleSets.lean b/LeanByExample/Declarative/DeclareAesopRuleSets.lean index 0c00ab4a..f3e5cf27 100644 --- a/LeanByExample/Declarative/DeclareAesopRuleSets.lean +++ b/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 diff --git a/LeanByExample/Declarative/DeclareAesopRuleSetsLib.lean b/LeanByExample/Declarative/DeclareAesopRuleSetsLib.lean index da2b4097..e8ec2295 100644 --- a/LeanByExample/Declarative/DeclareAesopRuleSetsLib.lean +++ b/LeanByExample/Declarative/DeclareAesopRuleSetsLib.lean @@ -1,3 +1,4 @@ +-- import されているファイルの内容 import Aesop declare_aesop_rule_sets [HogeRules]