Merge pull request #953 from lean-ja/changeDir

ディレクトリ名変更: `Examples` → `LeanByExample`
lean-ja · Oct 6, 2024 · 353f081 · 353f081
2 parents e2c9f83 + bcc2ab1
commit 353f081
Show file tree

Hide file tree

Showing 178 changed files with 17 additions and 14 deletions.
diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md
@@ -16,7 +16,7 @@
 ## 開発の流れ
 
 * このリポジトリは mathlib に依存しているので、このリポジトリを clone した後に `lake exe cache get` を実行してください。
-* `Exercise` ディレクトリ配下のファイルは `mk_exercise` により `Examples/Solution` の内容から自動生成されるので、手動で編集しないでください。
+* `Exercise` ディレクトリ配下のファイルは `mk_exercise` により `LeanByExample/Solution` の内容から自動生成されるので、手動で編集しないでください。
 * 本文の markdown ファイルは [mdgen](https://github.com/Seasawher/mdgen) を用いて Lean ファイルから生成します。Lean ファイルを編集した後、`lake run build` コマンドを実行すれば mk_exercise の実行と markdown の生成と `mdbook build` が一括実行されます。
 
 ## ルール
@@ -25,7 +25,7 @@
 * 読点には `、` を、句点には `。` を使用します。ただし例外として、直前の文字が半角文字であるときには `、` の代わりに半角カンマ `,` を使用します。
 * 見出し語 `foo` に対して、目次の中での記事の名前は `foo: (日本語による一言説明)` とします。可能な限り１行に収まるようにしてください。
 * 目次である `booksrc/SUMMARY.md` の内の記事は、カテゴリごとにアルファベット昇順に並べてください。VSCode だと [Tyriar.sort-lines](https://marketplace.visualstudio.com/items?itemName=Tyriar.sort-lines) という拡張機能があって、並び替えを自動で行うことができます。
-* Lean コードは、コンパイルが通るようにして `Examples` 配下に配置します。
+* Lean コードは、コンパイルが通るようにして `LeanByExample` 配下に配置します。
   * 「エラーになる例」を紹介したいときであっても `try` や `#guard_msgs` や `fail_if_success` などを使ってコンパイルが通るようにしてください。コード例が正しいかチェックする際にその方が楽だからです。
   * Lean ファイルのファイル名は、パスカルケースで命名して下さい。
   * ただしファイル名は、`README` 以外は大文字が連続しないようにします。
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -36,7 +36,7 @@
   "material-icon-theme.folders.associations": {
     "booksrc": "markdown",
     "Command": "",
-    "Examples": "Content",
+    "LeanByExample": "Content",
     "Option": "",
   },
 

diff --git a/Examples/Attribute/AppUnexpander.lean → LeanByExample/Attribute/AppUnexpander.lean b/Examples/Attribute/AppUnexpander.lean → LeanByExample/Attribute/AppUnexpander.lean
diff --git a/Examples/Attribute/CasesEliminator.lean → LeanByExample/Attribute/CasesEliminator.lean b/Examples/Attribute/CasesEliminator.lean → LeanByExample/Attribute/CasesEliminator.lean
diff --git a/Examples/Attribute/Coe.lean → LeanByExample/Attribute/Coe.lean b/Examples/Attribute/Coe.lean → LeanByExample/Attribute/Coe.lean
diff --git a/Examples/Attribute/Csimp.lean → LeanByExample/Attribute/Csimp.lean b/Examples/Attribute/Csimp.lean → LeanByExample/Attribute/Csimp.lean
diff --git a/Examples/Attribute/DefaultInstance.lean → LeanByExample/Attribute/DefaultInstance.lean b/Examples/Attribute/DefaultInstance.lean → LeanByExample/Attribute/DefaultInstance.lean
diff --git a/Examples/Attribute/InductionEliminator.lean → ...xample/Attribute/InductionEliminator.lean b/Examples/Attribute/InductionEliminator.lean → ...xample/Attribute/InductionEliminator.lean
diff --git a/Examples/Attribute/InheritDoc.lean → LeanByExample/Attribute/InheritDoc.lean b/Examples/Attribute/InheritDoc.lean → LeanByExample/Attribute/InheritDoc.lean
diff --git a/Examples/Attribute/MatchPattern.lean → LeanByExample/Attribute/MatchPattern.lean b/Examples/Attribute/MatchPattern.lean → LeanByExample/Attribute/MatchPattern.lean
diff --git a/Examples/Attribute/README.lean → LeanByExample/Attribute/README.lean b/Examples/Attribute/README.lean → LeanByExample/Attribute/README.lean
diff --git a/Examples/Attribute/Simps.lean → LeanByExample/Attribute/Simps.lean b/Examples/Attribute/Simps.lean → LeanByExample/Attribute/Simps.lean
diff --git a/Examples/Declarative/Abbrev.lean → LeanByExample/Declarative/Abbrev.lean b/Examples/Declarative/Abbrev.lean → LeanByExample/Declarative/Abbrev.lean
diff --git a/Examples/Declarative/AddAesopRules.lean → LeanByExample/Declarative/AddAesopRules.lean b/Examples/Declarative/AddAesopRules.lean → LeanByExample/Declarative/AddAesopRules.lean
diff --git a/Examples/Declarative/Attribute.lean → LeanByExample/Declarative/Attribute.lean b/Examples/Declarative/Attribute.lean → LeanByExample/Declarative/Attribute.lean
diff --git a/Examples/Declarative/Axiom.lean → LeanByExample/Declarative/Axiom.lean b/Examples/Declarative/Axiom.lean → LeanByExample/Declarative/Axiom.lean
diff --git a/Examples/Declarative/Class.lean → LeanByExample/Declarative/Class.lean b/Examples/Declarative/Class.lean → LeanByExample/Declarative/Class.lean
diff --git a/Examples/Declarative/DeclareSyntaxCat.lean → ...Example/Declarative/DeclareSyntaxCat.lean b/Examples/Declarative/DeclareSyntaxCat.lean → ...Example/Declarative/DeclareSyntaxCat.lean
diff --git a/Examples/Declarative/Def.lean → LeanByExample/Declarative/Def.lean b/Examples/Declarative/Def.lean → LeanByExample/Declarative/Def.lean
diff --git a/Examples/Declarative/Deriving.lean → LeanByExample/Declarative/Deriving.lean b/Examples/Declarative/Deriving.lean → LeanByExample/Declarative/Deriving.lean
diff --git a/Examples/Declarative/Elab.lean → LeanByExample/Declarative/Elab.lean b/Examples/Declarative/Elab.lean → LeanByExample/Declarative/Elab.lean
diff --git a/Examples/Declarative/Example.lean → LeanByExample/Declarative/Example.lean b/Examples/Declarative/Example.lean → LeanByExample/Declarative/Example.lean
diff --git a/Examples/Declarative/Export.lean → LeanByExample/Declarative/Export.lean b/Examples/Declarative/Export.lean → LeanByExample/Declarative/Export.lean
diff --git a/Examples/Declarative/Inductive.lean → LeanByExample/Declarative/Inductive.lean b/Examples/Declarative/Inductive.lean → LeanByExample/Declarative/Inductive.lean
diff --git a/Examples/Declarative/Infix.lean → LeanByExample/Declarative/Infix.lean b/Examples/Declarative/Infix.lean → LeanByExample/Declarative/Infix.lean
diff --git a/Examples/Declarative/Instance.lean → LeanByExample/Declarative/Instance.lean b/Examples/Declarative/Instance.lean → LeanByExample/Declarative/Instance.lean
diff --git a/Examples/Declarative/Local.lean → LeanByExample/Declarative/Local.lean b/Examples/Declarative/Local.lean → LeanByExample/Declarative/Local.lean
diff --git a/Examples/Declarative/Macro.lean → LeanByExample/Declarative/Macro.lean b/Examples/Declarative/Macro.lean → LeanByExample/Declarative/Macro.lean
diff --git a/Examples/Declarative/MacroRules.lean → LeanByExample/Declarative/MacroRules.lean b/Examples/Declarative/MacroRules.lean → LeanByExample/Declarative/MacroRules.lean
diff --git a/Examples/Declarative/Namespace.lean → LeanByExample/Declarative/Namespace.lean b/Examples/Declarative/Namespace.lean → LeanByExample/Declarative/Namespace.lean
diff --git a/Examples/Declarative/Noncomputable.lean → LeanByExample/Declarative/Noncomputable.lean b/Examples/Declarative/Noncomputable.lean → LeanByExample/Declarative/Noncomputable.lean
diff --git a/Examples/Declarative/Notation.lean → LeanByExample/Declarative/Notation.lean b/Examples/Declarative/Notation.lean → LeanByExample/Declarative/Notation.lean
diff --git a/Examples/Declarative/Opaque.lean → LeanByExample/Declarative/Opaque.lean b/Examples/Declarative/Opaque.lean → LeanByExample/Declarative/Opaque.lean
diff --git a/Examples/Declarative/Open.lean → LeanByExample/Declarative/Open.lean b/Examples/Declarative/Open.lean → LeanByExample/Declarative/Open.lean
diff --git a/Examples/Declarative/Partial.lean → LeanByExample/Declarative/Partial.lean b/Examples/Declarative/Partial.lean → LeanByExample/Declarative/Partial.lean
diff --git a/Examples/Declarative/Postfix.lean → LeanByExample/Declarative/Postfix.lean b/Examples/Declarative/Postfix.lean → LeanByExample/Declarative/Postfix.lean
diff --git a/Examples/Declarative/Prefix.lean → LeanByExample/Declarative/Prefix.lean b/Examples/Declarative/Prefix.lean → LeanByExample/Declarative/Prefix.lean
diff --git a/Examples/Declarative/Private.lean → LeanByExample/Declarative/Private.lean b/Examples/Declarative/Private.lean → LeanByExample/Declarative/Private.lean
diff --git a/Examples/Declarative/ProofWanted.lean → LeanByExample/Declarative/ProofWanted.lean b/Examples/Declarative/ProofWanted.lean → LeanByExample/Declarative/ProofWanted.lean
diff --git a/Examples/Declarative/Protected.lean → LeanByExample/Declarative/Protected.lean b/Examples/Declarative/Protected.lean → LeanByExample/Declarative/Protected.lean
diff --git a/Examples/Declarative/README.lean → LeanByExample/Declarative/README.lean b/Examples/Declarative/README.lean → LeanByExample/Declarative/README.lean
diff --git a/Examples/Declarative/Scoped.lean → LeanByExample/Declarative/Scoped.lean b/Examples/Declarative/Scoped.lean → LeanByExample/Declarative/Scoped.lean
diff --git a/Examples/Declarative/Section.lean → LeanByExample/Declarative/Section.lean b/Examples/Declarative/Section.lean → LeanByExample/Declarative/Section.lean
diff --git a/Examples/Declarative/SetOption.lean → LeanByExample/Declarative/SetOption.lean b/Examples/Declarative/SetOption.lean → LeanByExample/Declarative/SetOption.lean
diff --git a/Examples/Declarative/Structure.lean → LeanByExample/Declarative/Structure.lean b/Examples/Declarative/Structure.lean → LeanByExample/Declarative/Structure.lean
diff --git a/Examples/Declarative/Syntax.lean → LeanByExample/Declarative/Syntax.lean b/Examples/Declarative/Syntax.lean → LeanByExample/Declarative/Syntax.lean
diff --git a/Examples/Declarative/TerminationBy.lean → LeanByExample/Declarative/TerminationBy.lean b/Examples/Declarative/TerminationBy.lean → LeanByExample/Declarative/TerminationBy.lean
diff --git a/Examples/Declarative/Theorem.lean → LeanByExample/Declarative/Theorem.lean b/Examples/Declarative/Theorem.lean → LeanByExample/Declarative/Theorem.lean
diff --git a/Examples/Declarative/Variable.lean → LeanByExample/Declarative/Variable.lean b/Examples/Declarative/Variable.lean → LeanByExample/Declarative/Variable.lean
diff --git a/Examples/Diagnostic/Check.lean → LeanByExample/Diagnostic/Check.lean b/Examples/Diagnostic/Check.lean → LeanByExample/Diagnostic/Check.lean
diff --git a/Examples/Diagnostic/CheckFailure.lean → LeanByExample/Diagnostic/CheckFailure.lean b/Examples/Diagnostic/CheckFailure.lean → LeanByExample/Diagnostic/CheckFailure.lean
diff --git a/Examples/Diagnostic/Eval.lean → LeanByExample/Diagnostic/Eval.lean b/Examples/Diagnostic/Eval.lean → LeanByExample/Diagnostic/Eval.lean
diff --git a/Examples/Diagnostic/Find.lean → LeanByExample/Diagnostic/Find.lean b/Examples/Diagnostic/Find.lean → LeanByExample/Diagnostic/Find.lean
diff --git a/Examples/Diagnostic/Guard.lean → LeanByExample/Diagnostic/Guard.lean b/Examples/Diagnostic/Guard.lean → LeanByExample/Diagnostic/Guard.lean
diff --git a/Examples/Diagnostic/GuardMsgs.lean → LeanByExample/Diagnostic/GuardMsgs.lean b/Examples/Diagnostic/GuardMsgs.lean → LeanByExample/Diagnostic/GuardMsgs.lean
diff --git a/Examples/Diagnostic/Help.lean → LeanByExample/Diagnostic/Help.lean b/Examples/Diagnostic/Help.lean → LeanByExample/Diagnostic/Help.lean
diff --git a/Examples/Diagnostic/Instances.lean → LeanByExample/Diagnostic/Instances.lean b/Examples/Diagnostic/Instances.lean → LeanByExample/Diagnostic/Instances.lean
diff --git a/Examples/Diagnostic/Print.lean → LeanByExample/Diagnostic/Print.lean b/Examples/Diagnostic/Print.lean → LeanByExample/Diagnostic/Print.lean
diff --git a/Examples/Diagnostic/README.lean → LeanByExample/Diagnostic/README.lean b/Examples/Diagnostic/README.lean → LeanByExample/Diagnostic/README.lean
diff --git a/Examples/Diagnostic/Reduce.lean → LeanByExample/Diagnostic/Reduce.lean b/Examples/Diagnostic/Reduce.lean → LeanByExample/Diagnostic/Reduce.lean
diff --git a/Examples/Diagnostic/Synth.lean → LeanByExample/Diagnostic/Synth.lean b/Examples/Diagnostic/Synth.lean → LeanByExample/Diagnostic/Synth.lean
diff --git a/Examples/Diagnostic/Time.lean → LeanByExample/Diagnostic/Time.lean b/Examples/Diagnostic/Time.lean → LeanByExample/Diagnostic/Time.lean
diff --git a/Examples/Diagnostic/Whnf.lean → LeanByExample/Diagnostic/Whnf.lean b/Examples/Diagnostic/Whnf.lean → LeanByExample/Diagnostic/Whnf.lean
diff --git a/Examples/Option/AutoImplicit.lean → LeanByExample/Option/AutoImplicit.lean b/Examples/Option/AutoImplicit.lean → LeanByExample/Option/AutoImplicit.lean
diff --git a/Examples/Option/Flexible.lean → LeanByExample/Option/Flexible.lean b/Examples/Option/Flexible.lean → LeanByExample/Option/Flexible.lean
diff --git a/Examples/Option/Hygiene.lean → LeanByExample/Option/Hygiene.lean b/Examples/Option/Hygiene.lean → LeanByExample/Option/Hygiene.lean
diff --git a/Examples/Option/README.lean → LeanByExample/Option/README.lean b/Examples/Option/README.lean → LeanByExample/Option/README.lean
diff --git a/Examples/Solution/BarberParadox.lean → LeanByExample/Solution/BarberParadox.lean b/Examples/Solution/BarberParadox.lean → LeanByExample/Solution/BarberParadox.lean
diff --git a/Examples/Solution/CantorPairing.lean → LeanByExample/Solution/CantorPairing.lean b/Examples/Solution/CantorPairing.lean → LeanByExample/Solution/CantorPairing.lean
diff --git a/Examples/Solution/CantorTheorem.lean → LeanByExample/Solution/CantorTheorem.lean b/Examples/Solution/CantorTheorem.lean → LeanByExample/Solution/CantorTheorem.lean
diff --git a/Examples/Solution/DoubtImplication.lean → LeanByExample/Solution/DoubtImplication.lean b/Examples/Solution/DoubtImplication.lean → LeanByExample/Solution/DoubtImplication.lean
diff --git a/...es/Solution/HeytingAndBooleanAlgebra.lean → ...le/Solution/HeytingAndBooleanAlgebra.lean b/...es/Solution/HeytingAndBooleanAlgebra.lean → ...le/Solution/HeytingAndBooleanAlgebra.lean
diff --git a/Examples/Solution/InverseSurjInj.lean → LeanByExample/Solution/InverseSurjInj.lean b/Examples/Solution/InverseSurjInj.lean → LeanByExample/Solution/InverseSurjInj.lean
diff --git a/Examples/Solution/KnightAndKnave.lean → LeanByExample/Solution/KnightAndKnave.lean b/Examples/Solution/KnightAndKnave.lean → LeanByExample/Solution/KnightAndKnave.lean
diff --git a/Examples/Solution/README.lean → LeanByExample/Solution/README.lean b/Examples/Solution/README.lean → LeanByExample/Solution/README.lean
diff --git a/Examples/Tactic/AcRfl.lean → LeanByExample/Tactic/AcRfl.lean b/Examples/Tactic/AcRfl.lean → LeanByExample/Tactic/AcRfl.lean
diff --git a/Examples/Tactic/Aesop.lean → LeanByExample/Tactic/Aesop.lean b/Examples/Tactic/Aesop.lean → LeanByExample/Tactic/Aesop.lean
diff --git a/Examples/Tactic/AllGoals.lean → LeanByExample/Tactic/AllGoals.lean b/Examples/Tactic/AllGoals.lean → LeanByExample/Tactic/AllGoals.lean
diff --git a/Examples/Tactic/Apply.lean → LeanByExample/Tactic/Apply.lean b/Examples/Tactic/Apply.lean → LeanByExample/Tactic/Apply.lean
diff --git a/Examples/Tactic/ApplyAssumption.lean → LeanByExample/Tactic/ApplyAssumption.lean b/Examples/Tactic/ApplyAssumption.lean → LeanByExample/Tactic/ApplyAssumption.lean
diff --git a/Examples/Tactic/ApplyAt.lean → LeanByExample/Tactic/ApplyAt.lean b/Examples/Tactic/ApplyAt.lean → LeanByExample/Tactic/ApplyAt.lean
diff --git a/Examples/Tactic/ApplyQuestion.lean → LeanByExample/Tactic/ApplyQuestion.lean b/Examples/Tactic/ApplyQuestion.lean → LeanByExample/Tactic/ApplyQuestion.lean
diff --git a/Examples/Tactic/Assumption.lean → LeanByExample/Tactic/Assumption.lean b/Examples/Tactic/Assumption.lean → LeanByExample/Tactic/Assumption.lean
diff --git a/Examples/Tactic/By.lean → LeanByExample/Tactic/By.lean b/Examples/Tactic/By.lean → LeanByExample/Tactic/By.lean
diff --git a/Examples/Tactic/ByCases.lean → LeanByExample/Tactic/ByCases.lean b/Examples/Tactic/ByCases.lean → LeanByExample/Tactic/ByCases.lean
diff --git a/Examples/Tactic/ByContra.lean → LeanByExample/Tactic/ByContra.lean b/Examples/Tactic/ByContra.lean → LeanByExample/Tactic/ByContra.lean
diff --git a/Examples/Tactic/Calc.lean → LeanByExample/Tactic/Calc.lean b/Examples/Tactic/Calc.lean → LeanByExample/Tactic/Calc.lean
diff --git a/Examples/Tactic/Cases.lean → LeanByExample/Tactic/Cases.lean b/Examples/Tactic/Cases.lean → LeanByExample/Tactic/Cases.lean
diff --git a/Examples/Tactic/CasesAp.lean → LeanByExample/Tactic/CasesAp.lean b/Examples/Tactic/CasesAp.lean → LeanByExample/Tactic/CasesAp.lean
diff --git a/Examples/Tactic/Choose.lean → LeanByExample/Tactic/Choose.lean b/Examples/Tactic/Choose.lean → LeanByExample/Tactic/Choose.lean
diff --git a/Examples/Tactic/Clear.lean → LeanByExample/Tactic/Clear.lean b/Examples/Tactic/Clear.lean → LeanByExample/Tactic/Clear.lean
diff --git a/Examples/Tactic/Congr.lean → LeanByExample/Tactic/Congr.lean b/Examples/Tactic/Congr.lean → LeanByExample/Tactic/Congr.lean
diff --git a/Examples/Tactic/Constructor.lean → LeanByExample/Tactic/Constructor.lean b/Examples/Tactic/Constructor.lean → LeanByExample/Tactic/Constructor.lean
diff --git a/Examples/Tactic/Contradiction.lean → LeanByExample/Tactic/Contradiction.lean b/Examples/Tactic/Contradiction.lean → LeanByExample/Tactic/Contradiction.lean
diff --git a/Examples/Tactic/Contrapose.lean → LeanByExample/Tactic/Contrapose.lean b/Examples/Tactic/Contrapose.lean → LeanByExample/Tactic/Contrapose.lean
diff --git a/Examples/Tactic/Conv.lean → LeanByExample/Tactic/Conv.lean b/Examples/Tactic/Conv.lean → LeanByExample/Tactic/Conv.lean
diff --git a/Examples/Tactic/Convert.lean → LeanByExample/Tactic/Convert.lean b/Examples/Tactic/Convert.lean → LeanByExample/Tactic/Convert.lean
diff --git a/Examples/Tactic/Decide.lean → LeanByExample/Tactic/Decide.lean b/Examples/Tactic/Decide.lean → LeanByExample/Tactic/Decide.lean
diff --git a/Examples/Tactic/Done.lean → LeanByExample/Tactic/Done.lean b/Examples/Tactic/Done.lean → LeanByExample/Tactic/Done.lean
diff --git a/Examples/Tactic/Dsimp.lean → LeanByExample/Tactic/Dsimp.lean b/Examples/Tactic/Dsimp.lean → LeanByExample/Tactic/Dsimp.lean
diff --git a/Examples/Tactic/Exact.lean → LeanByExample/Tactic/Exact.lean b/Examples/Tactic/Exact.lean → LeanByExample/Tactic/Exact.lean
diff --git a/Examples/Tactic/ExactQuestion.lean → LeanByExample/Tactic/ExactQuestion.lean b/Examples/Tactic/ExactQuestion.lean → LeanByExample/Tactic/ExactQuestion.lean
diff --git a/Examples/Tactic/Exfalso.lean → LeanByExample/Tactic/Exfalso.lean b/Examples/Tactic/Exfalso.lean → LeanByExample/Tactic/Exfalso.lean
diff --git a/Examples/Tactic/Exists.lean → LeanByExample/Tactic/Exists.lean b/Examples/Tactic/Exists.lean → LeanByExample/Tactic/Exists.lean
diff --git a/Examples/Tactic/Ext.lean → LeanByExample/Tactic/Ext.lean b/Examples/Tactic/Ext.lean → LeanByExample/Tactic/Ext.lean
diff --git a/Examples/Tactic/FieldSimp.lean → LeanByExample/Tactic/FieldSimp.lean b/Examples/Tactic/FieldSimp.lean → LeanByExample/Tactic/FieldSimp.lean
diff --git a/Examples/Tactic/FinCases.lean → LeanByExample/Tactic/FinCases.lean b/Examples/Tactic/FinCases.lean → LeanByExample/Tactic/FinCases.lean
diff --git a/Examples/Tactic/FunProp.lean → LeanByExample/Tactic/FunProp.lean b/Examples/Tactic/FunProp.lean → LeanByExample/Tactic/FunProp.lean
diff --git a/Examples/Tactic/Funext.lean → LeanByExample/Tactic/Funext.lean b/Examples/Tactic/Funext.lean → LeanByExample/Tactic/Funext.lean
diff --git a/Examples/Tactic/Gcongr.lean → LeanByExample/Tactic/Gcongr.lean b/Examples/Tactic/Gcongr.lean → LeanByExample/Tactic/Gcongr.lean
diff --git a/Examples/Tactic/Generalize.lean → LeanByExample/Tactic/Generalize.lean b/Examples/Tactic/Generalize.lean → LeanByExample/Tactic/Generalize.lean
diff --git a/Examples/Tactic/GuardHyp.lean → LeanByExample/Tactic/GuardHyp.lean b/Examples/Tactic/GuardHyp.lean → LeanByExample/Tactic/GuardHyp.lean
diff --git a/Examples/Tactic/Have.lean → LeanByExample/Tactic/Have.lean b/Examples/Tactic/Have.lean → LeanByExample/Tactic/Have.lean
diff --git a/Examples/Tactic/Hint.lean → LeanByExample/Tactic/Hint.lean b/Examples/Tactic/Hint.lean → LeanByExample/Tactic/Hint.lean
diff --git a/Examples/Tactic/Induction.lean → LeanByExample/Tactic/Induction.lean b/Examples/Tactic/Induction.lean → LeanByExample/Tactic/Induction.lean
diff --git a/Examples/Tactic/InductionAp.lean → LeanByExample/Tactic/InductionAp.lean b/Examples/Tactic/InductionAp.lean → LeanByExample/Tactic/InductionAp.lean
diff --git a/Examples/Tactic/Intro.lean → LeanByExample/Tactic/Intro.lean b/Examples/Tactic/Intro.lean → LeanByExample/Tactic/Intro.lean
diff --git a/Examples/Tactic/Itauto.lean → LeanByExample/Tactic/Itauto.lean b/Examples/Tactic/Itauto.lean → LeanByExample/Tactic/Itauto.lean
diff --git a/Examples/Tactic/Left.lean → LeanByExample/Tactic/Left.lean b/Examples/Tactic/Left.lean → LeanByExample/Tactic/Left.lean
diff --git a/Examples/Tactic/Linarith.lean → LeanByExample/Tactic/Linarith.lean b/Examples/Tactic/Linarith.lean → LeanByExample/Tactic/Linarith.lean
diff --git a/Examples/Tactic/NativeDecide.lean → LeanByExample/Tactic/NativeDecide.lean b/Examples/Tactic/NativeDecide.lean → LeanByExample/Tactic/NativeDecide.lean
diff --git a/Examples/Tactic/Nlinarith.lean → LeanByExample/Tactic/Nlinarith.lean b/Examples/Tactic/Nlinarith.lean → LeanByExample/Tactic/Nlinarith.lean
diff --git a/Examples/Tactic/NormCast.lean → LeanByExample/Tactic/NormCast.lean b/Examples/Tactic/NormCast.lean → LeanByExample/Tactic/NormCast.lean
diff --git a/Examples/Tactic/NthRw.lean → LeanByExample/Tactic/NthRw.lean b/Examples/Tactic/NthRw.lean → LeanByExample/Tactic/NthRw.lean
diff --git a/Examples/Tactic/Obtain.lean → LeanByExample/Tactic/Obtain.lean b/Examples/Tactic/Obtain.lean → LeanByExample/Tactic/Obtain.lean
diff --git a/Examples/Tactic/Omega.lean → LeanByExample/Tactic/Omega.lean b/Examples/Tactic/Omega.lean → LeanByExample/Tactic/Omega.lean
diff --git a/Examples/Tactic/Positivity.lean → LeanByExample/Tactic/Positivity.lean b/Examples/Tactic/Positivity.lean → LeanByExample/Tactic/Positivity.lean
diff --git a/Examples/Tactic/PushNeg.lean → LeanByExample/Tactic/PushNeg.lean b/Examples/Tactic/PushNeg.lean → LeanByExample/Tactic/PushNeg.lean
diff --git a/Examples/Tactic/Qify.lean → LeanByExample/Tactic/Qify.lean b/Examples/Tactic/Qify.lean → LeanByExample/Tactic/Qify.lean
diff --git a/Examples/Tactic/README.lean → LeanByExample/Tactic/README.lean b/Examples/Tactic/README.lean → LeanByExample/Tactic/README.lean
diff --git a/Examples/Tactic/Rcases.lean → LeanByExample/Tactic/Rcases.lean b/Examples/Tactic/Rcases.lean → LeanByExample/Tactic/Rcases.lean
diff --git a/Examples/Tactic/Refine.lean → LeanByExample/Tactic/Refine.lean b/Examples/Tactic/Refine.lean → LeanByExample/Tactic/Refine.lean
diff --git a/Examples/Tactic/Rel.lean → LeanByExample/Tactic/Rel.lean b/Examples/Tactic/Rel.lean → LeanByExample/Tactic/Rel.lean
diff --git a/Examples/Tactic/RenameI.lean → LeanByExample/Tactic/RenameI.lean b/Examples/Tactic/RenameI.lean → LeanByExample/Tactic/RenameI.lean
diff --git a/Examples/Tactic/Repeat.lean → LeanByExample/Tactic/Repeat.lean b/Examples/Tactic/Repeat.lean → LeanByExample/Tactic/Repeat.lean
diff --git a/Examples/Tactic/Replace.lean → LeanByExample/Tactic/Replace.lean b/Examples/Tactic/Replace.lean → LeanByExample/Tactic/Replace.lean
diff --git a/Examples/Tactic/Rfl.lean → LeanByExample/Tactic/Rfl.lean b/Examples/Tactic/Rfl.lean → LeanByExample/Tactic/Rfl.lean
diff --git a/Examples/Tactic/Right.lean → LeanByExample/Tactic/Right.lean b/Examples/Tactic/Right.lean → LeanByExample/Tactic/Right.lean
diff --git a/Examples/Tactic/Ring.lean → LeanByExample/Tactic/Ring.lean b/Examples/Tactic/Ring.lean → LeanByExample/Tactic/Ring.lean
diff --git a/Examples/Tactic/Rw.lean → LeanByExample/Tactic/Rw.lean b/Examples/Tactic/Rw.lean → LeanByExample/Tactic/Rw.lean
diff --git a/Examples/Tactic/RwSearch.lean → LeanByExample/Tactic/RwSearch.lean b/Examples/Tactic/RwSearch.lean → LeanByExample/Tactic/RwSearch.lean
diff --git a/Examples/Tactic/Says.lean → LeanByExample/Tactic/Says.lean b/Examples/Tactic/Says.lean → LeanByExample/Tactic/Says.lean
diff --git a/Examples/Tactic/SeqFocus.lean → LeanByExample/Tactic/SeqFocus.lean b/Examples/Tactic/SeqFocus.lean → LeanByExample/Tactic/SeqFocus.lean
diff --git a/Examples/Tactic/Set.lean → LeanByExample/Tactic/Set.lean b/Examples/Tactic/Set.lean → LeanByExample/Tactic/Set.lean
diff --git a/Examples/Tactic/Show.lean → LeanByExample/Tactic/Show.lean b/Examples/Tactic/Show.lean → LeanByExample/Tactic/Show.lean
diff --git a/Examples/Tactic/Simp.lean → LeanByExample/Tactic/Simp.lean b/Examples/Tactic/Simp.lean → LeanByExample/Tactic/Simp.lean
diff --git a/Examples/Tactic/SlimCheck.lean → LeanByExample/Tactic/SlimCheck.lean b/Examples/Tactic/SlimCheck.lean → LeanByExample/Tactic/SlimCheck.lean
diff --git a/Examples/Tactic/Sorry.lean → LeanByExample/Tactic/Sorry.lean b/Examples/Tactic/Sorry.lean → LeanByExample/Tactic/Sorry.lean
diff --git a/Examples/Tactic/Split.lean → LeanByExample/Tactic/Split.lean b/Examples/Tactic/Split.lean → LeanByExample/Tactic/Split.lean
diff --git a/Examples/Tactic/Suffices.lean → LeanByExample/Tactic/Suffices.lean b/Examples/Tactic/Suffices.lean → LeanByExample/Tactic/Suffices.lean
diff --git a/Examples/Tactic/Tauto.lean → LeanByExample/Tactic/Tauto.lean b/Examples/Tactic/Tauto.lean → LeanByExample/Tactic/Tauto.lean
diff --git a/Examples/Tactic/Trans.lean → LeanByExample/Tactic/Trans.lean b/Examples/Tactic/Trans.lean → LeanByExample/Tactic/Trans.lean
diff --git a/Examples/Tactic/Trivial.lean → LeanByExample/Tactic/Trivial.lean b/Examples/Tactic/Trivial.lean → LeanByExample/Tactic/Trivial.lean
diff --git a/Examples/Tactic/Try.lean → LeanByExample/Tactic/Try.lean b/Examples/Tactic/Try.lean → LeanByExample/Tactic/Try.lean
diff --git a/Examples/Tactic/Unfold.lean → LeanByExample/Tactic/Unfold.lean b/Examples/Tactic/Unfold.lean → LeanByExample/Tactic/Unfold.lean
diff --git a/Examples/Tactic/WithReducible.lean → LeanByExample/Tactic/WithReducible.lean b/Examples/Tactic/WithReducible.lean → LeanByExample/Tactic/WithReducible.lean
diff --git a/Examples/Tactic/Wlog.lean → LeanByExample/Tactic/Wlog.lean b/Examples/Tactic/Wlog.lean → LeanByExample/Tactic/Wlog.lean
diff --git a/Examples/Type/Char.lean → LeanByExample/Type/Char.lean b/Examples/Type/Char.lean → LeanByExample/Type/Char.lean
diff --git a/Examples/Type/Float.lean → LeanByExample/Type/Float.lean b/Examples/Type/Float.lean → LeanByExample/Type/Float.lean
diff --git a/Examples/Type/List.lean → LeanByExample/Type/List.lean b/Examples/Type/List.lean → LeanByExample/Type/List.lean
diff --git a/Examples/Type/Prop.lean → LeanByExample/Type/Prop.lean b/Examples/Type/Prop.lean → LeanByExample/Type/Prop.lean
diff --git a/Examples/Type/README.lean → LeanByExample/Type/README.lean b/Examples/Type/README.lean → LeanByExample/Type/README.lean
diff --git a/Examples/Type/String.lean → LeanByExample/Type/String.lean b/Examples/Type/String.lean → LeanByExample/Type/String.lean
diff --git a/Examples/Type/Type.lean → LeanByExample/Type/Type.lean b/Examples/Type/Type.lean → LeanByExample/Type/Type.lean
diff --git a/Examples/TypeClass/Coe.lean → LeanByExample/TypeClass/Coe.lean b/Examples/TypeClass/Coe.lean → LeanByExample/TypeClass/Coe.lean
diff --git a/Examples/TypeClass/CoeDep.lean → LeanByExample/TypeClass/CoeDep.lean b/Examples/TypeClass/CoeDep.lean → LeanByExample/TypeClass/CoeDep.lean
diff --git a/Examples/TypeClass/CoeFun.lean → LeanByExample/TypeClass/CoeFun.lean b/Examples/TypeClass/CoeFun.lean → LeanByExample/TypeClass/CoeFun.lean
diff --git a/Examples/TypeClass/CoeSort.lean → LeanByExample/TypeClass/CoeSort.lean b/Examples/TypeClass/CoeSort.lean → LeanByExample/TypeClass/CoeSort.lean
diff --git a/Examples/TypeClass/Decidable.lean → LeanByExample/TypeClass/Decidable.lean b/Examples/TypeClass/Decidable.lean → LeanByExample/TypeClass/Decidable.lean
diff --git a/Examples/TypeClass/GetElem.lean → LeanByExample/TypeClass/GetElem.lean b/Examples/TypeClass/GetElem.lean → LeanByExample/TypeClass/GetElem.lean
diff --git a/Examples/TypeClass/Inhabited.lean → LeanByExample/TypeClass/Inhabited.lean b/Examples/TypeClass/Inhabited.lean → LeanByExample/TypeClass/Inhabited.lean
diff --git a/Examples/TypeClass/OfNat.lean → LeanByExample/TypeClass/OfNat.lean b/Examples/TypeClass/OfNat.lean → LeanByExample/TypeClass/OfNat.lean
diff --git a/Examples/TypeClass/README.lean → LeanByExample/TypeClass/README.lean b/Examples/TypeClass/README.lean → LeanByExample/TypeClass/README.lean
diff --git a/Examples/TypeClass/Repr.lean → LeanByExample/TypeClass/Repr.lean b/Examples/TypeClass/Repr.lean → LeanByExample/TypeClass/Repr.lean
diff --git a/Examples/TypeClass/ToString.lean → LeanByExample/TypeClass/ToString.lean b/Examples/TypeClass/ToString.lean → LeanByExample/TypeClass/ToString.lean
diff --git a/assets/filePlay.js b/assets/filePlay.js
@@ -14,12 +14,15 @@ function filePlay() {
   // 拡張子が `.md` になっているので `.lean` に修正する
   editButtonLink.href = editButtonLink.href.replace(/\.md$/, ".lean");
 
-  // Lean ファイルがあるのは `booksrc` ではなく `Examples` ディレクトリ
-  editButtonLink.href = editButtonLink.href.replace("/booksrc/", "/Examples/");
+  // Lean ファイルがあるのは `booksrc` ではなく `LeanByExample` ディレクトリ
+  editButtonLink.href = editButtonLink.href.replace(
+    "/booksrc/",
+    "/LeanByExample/",
+  );
 
-  // 演習問題のファイルのみ、`Examples` ディレクトリではなくて `Exercise` ディレクトリにある
+  // 演習問題のファイルのみ、`LeanByExample` ディレクトリではなくて `Exercise` ディレクトリにある
   editButtonLink.href = editButtonLink.href.replace(
-    "/Examples/Exercise/",
+    "/LeanByExample/Exercise/",
     "/Exercise/",
   );
 

diff --git a/lakefile.lean b/lakefile.lean
@@ -21,10 +21,10 @@ require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @ "master"
 
 @[default_target]
-lean_lib Examples where
+lean_lib LeanByExample where
   -- `lake build` の実行時にビルドされるファイルの設定
   -- `.submodules` と指定すると、そのディレクトリ以下の全ての Lean ファイルがビルドされる
-  globs := #[.submodules `Examples]
+  globs := #[.submodules `LeanByExample]
 
 section Script
 
@@ -46,7 +46,7 @@ def runCmd (input : String) : IO Unit := do
 /-- mk_exercise を実行し、演習問題の解答に
 解答部分を sorry に置き換えるなどの処理を施して演習問題ファイルを生成する。-/
 script mk_exercise do
-  runCmd "lake exe mk_exercise Examples/Solution Exercise"
+  runCmd "lake exe mk_exercise LeanByExample/Solution Exercise"
   return 0
 
 syntax (name := with_time) "with_time" "running" str doElem : doElem
@@ -65,10 +65,10 @@ Lean ファイルから Markdown ファイルと HTML ファイルを生成す
 script build do
   -- `lake run mk_exercise` を使用すると遅くなってしまうのでコピペしている
   with_time running "mk_exercise"
-    runCmd "lake exe mk_exercise Examples/Solution Exercise"
+    runCmd "lake exe mk_exercise LeanByExample/Solution Exercise"
 
   with_time running "mdgen"
-    runCmd "lake exe mdgen Examples booksrc";
+    runCmd "lake exe mdgen LeanByExample booksrc";
     runCmd "lake exe mdgen Exercise booksrc/Exercise"
 
   with_time running "mdbook"

diff --git a/scripts/Build.ps1 b/scripts/Build.ps1
@@ -3,9 +3,9 @@
 lake を介することで実行が遅くなってしまうので、
 lake を介することなく実行ファイルを直接叩く。 #>
 
-./.lake/packages/mk-exercise/.lake/build/bin/mk_exercise.exe Examples/Solution Exercise
+./.lake/packages/mk-exercise/.lake/build/bin/mk_exercise.exe LeanByExample/Solution Exercise
 
 ./.lake/packages/mdgen/.lake/build/bin/mdgen.exe Exercise booksrc/Exercise
-./.lake/packages/mdgen/.lake/build/bin/mdgen.exe Examples booksrc
+./.lake/packages/mdgen/.lake/build/bin/mdgen.exe LeanByExample booksrc
 
 mdbook build