Merge pull request #954 from lean-ja/reorganize

ディレクトリ構成変更
lean-ja · Oct 7, 2024 · 049fef6 · 049fef6
2 parents 353f081 + 4dc783b
commit 049fef6
Show file tree

Hide file tree

Showing 188 changed files with 195 additions and 206 deletions.
diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md
@@ -16,7 +16,7 @@
 ## 開発の流れ
 
 * このリポジトリは mathlib に依存しているので、このリポジトリを clone した後に `lake exe cache get` を実行してください。
-* `Exercise` ディレクトリ配下のファイルは `mk_exercise` により `LeanByExample/Solution` の内容から自動生成されるので、手動で編集しないでください。
+* `LeanByExample/Tutorial/Exercise` ディレクトリ配下のファイルは `mk_exercise` により `LeanByExample/Solution` の内容から自動生成されるので、手動で編集しないでください。
 * 本文の markdown ファイルは [mdgen](https://github.com/Seasawher/mdgen) を用いて Lean ファイルから生成します。Lean ファイルを編集した後、`lake run build` コマンドを実行すれば mk_exercise の実行と markdown の生成と `mdbook build` が一括実行されます。
 
 ## ルール

diff --git a/.github/workflows/sync.yml b/.github/workflows/sync.yml
@@ -36,13 +36,13 @@ jobs:
       # いったん演習ファイルを全て削除している
       - name: run mk_exercise
         run: |
-          rm -r Exercise
-          lake run mk_exercise
+          rm -r LeanByExample/Tutorial/Exercise
+          lake exe mk_exercise LeanByExample/Tutorial/Solution LeanByExample/Tutorial/Exercise
 
       - name: detect diff
         id: diff
         run: |
-          git add -N Exercise
+          git add -N LeanByExample/Tutorial/Exercise
           git diff --name-only --exit-code
         continue-on-error: true
 
@@ -51,6 +51,6 @@ jobs:
         run: |
           git config user.name "GitHub Action"
           git config user.email "[email protected]"
-          git add Exercise
+          git add LeanByExample/Tutorial/Exercise
           git commit -m "generated by GitHub Action"
           git push origin HEAD:${{ github.event.pull_request.head.ref }}
diff --git a/LeanByExample/Attribute/AppUnexpander.lean → ...le/Reference/Attribute/AppUnexpander.lean b/LeanByExample/Attribute/AppUnexpander.lean → ...le/Reference/Attribute/AppUnexpander.lean
diff --git a/LeanByExample/Attribute/CasesEliminator.lean → .../Reference/Attribute/CasesEliminator.lean b/LeanByExample/Attribute/CasesEliminator.lean → .../Reference/Attribute/CasesEliminator.lean
diff --git a/LeanByExample/Attribute/Coe.lean → LeanByExample/Reference/Attribute/Coe.lean b/LeanByExample/Attribute/Coe.lean → LeanByExample/Reference/Attribute/Coe.lean
diff --git a/LeanByExample/Attribute/Csimp.lean → LeanByExample/Reference/Attribute/Csimp.lean b/LeanByExample/Attribute/Csimp.lean → LeanByExample/Reference/Attribute/Csimp.lean
diff --git a/LeanByExample/Attribute/DefaultInstance.lean → .../Reference/Attribute/DefaultInstance.lean b/LeanByExample/Attribute/DefaultInstance.lean → .../Reference/Attribute/DefaultInstance.lean
diff --git a/...xample/Attribute/InductionEliminator.lean → ...erence/Attribute/InductionEliminator.lean b/...xample/Attribute/InductionEliminator.lean → ...erence/Attribute/InductionEliminator.lean
diff --git a/LeanByExample/Attribute/InheritDoc.lean → ...ample/Reference/Attribute/InheritDoc.lean b/LeanByExample/Attribute/InheritDoc.lean → ...ample/Reference/Attribute/InheritDoc.lean
diff --git a/LeanByExample/Attribute/MatchPattern.lean → ...ple/Reference/Attribute/MatchPattern.lean b/LeanByExample/Attribute/MatchPattern.lean → ...ple/Reference/Attribute/MatchPattern.lean
diff --git a/LeanByExample/Attribute/README.lean → ...ByExample/Reference/Attribute/README.lean b/LeanByExample/Attribute/README.lean → ...ByExample/Reference/Attribute/README.lean
diff --git a/LeanByExample/Attribute/Simps.lean → LeanByExample/Reference/Attribute/Simps.lean b/LeanByExample/Attribute/Simps.lean → LeanByExample/Reference/Attribute/Simps.lean
diff --git a/LeanByExample/Declarative/Abbrev.lean → ...Example/Reference/Declarative/Abbrev.lean b/LeanByExample/Declarative/Abbrev.lean → ...Example/Reference/Declarative/Abbrev.lean
diff --git a/LeanByExample/Declarative/AddAesopRules.lean → .../Reference/Declarative/AddAesopRules.lean b/LeanByExample/Declarative/AddAesopRules.lean → .../Reference/Declarative/AddAesopRules.lean
diff --git a/LeanByExample/Declarative/Attribute.lean → ...mple/Reference/Declarative/Attribute.lean b/LeanByExample/Declarative/Attribute.lean → ...mple/Reference/Declarative/Attribute.lean
diff --git a/LeanByExample/Declarative/Axiom.lean → ...yExample/Reference/Declarative/Axiom.lean b/LeanByExample/Declarative/Axiom.lean → ...yExample/Reference/Declarative/Axiom.lean
diff --git a/LeanByExample/Declarative/Class.lean → ...yExample/Reference/Declarative/Class.lean b/LeanByExample/Declarative/Class.lean → ...yExample/Reference/Declarative/Class.lean
diff --git a/...Example/Declarative/DeclareSyntaxCat.lean → ...ference/Declarative/DeclareSyntaxCat.lean b/...Example/Declarative/DeclareSyntaxCat.lean → ...ference/Declarative/DeclareSyntaxCat.lean
diff --git a/LeanByExample/Declarative/Def.lean → LeanByExample/Reference/Declarative/Def.lean b/LeanByExample/Declarative/Def.lean → LeanByExample/Reference/Declarative/Def.lean
diff --git a/LeanByExample/Declarative/Deriving.lean → ...ample/Reference/Declarative/Deriving.lean b/LeanByExample/Declarative/Deriving.lean → ...ample/Reference/Declarative/Deriving.lean
diff --git a/LeanByExample/Declarative/Elab.lean → ...ByExample/Reference/Declarative/Elab.lean b/LeanByExample/Declarative/Elab.lean → ...ByExample/Reference/Declarative/Elab.lean
diff --git a/LeanByExample/Declarative/Example.lean → ...xample/Reference/Declarative/Example.lean b/LeanByExample/Declarative/Example.lean → ...xample/Reference/Declarative/Example.lean
diff --git a/LeanByExample/Declarative/Export.lean → ...Example/Reference/Declarative/Export.lean b/LeanByExample/Declarative/Export.lean → ...Example/Reference/Declarative/Export.lean
diff --git a/LeanByExample/Declarative/Inductive.lean → ...mple/Reference/Declarative/Inductive.lean b/LeanByExample/Declarative/Inductive.lean → ...mple/Reference/Declarative/Inductive.lean
diff --git a/LeanByExample/Declarative/Infix.lean → ...yExample/Reference/Declarative/Infix.lean b/LeanByExample/Declarative/Infix.lean → ...yExample/Reference/Declarative/Infix.lean
diff --git a/LeanByExample/Declarative/Instance.lean → ...ample/Reference/Declarative/Instance.lean b/LeanByExample/Declarative/Instance.lean → ...ample/Reference/Declarative/Instance.lean
diff --git a/LeanByExample/Declarative/Local.lean → ...yExample/Reference/Declarative/Local.lean b/LeanByExample/Declarative/Local.lean → ...yExample/Reference/Declarative/Local.lean
diff --git a/LeanByExample/Declarative/Macro.lean → ...yExample/Reference/Declarative/Macro.lean b/LeanByExample/Declarative/Macro.lean → ...yExample/Reference/Declarative/Macro.lean
diff --git a/LeanByExample/Declarative/MacroRules.lean → ...ple/Reference/Declarative/MacroRules.lean b/LeanByExample/Declarative/MacroRules.lean → ...ple/Reference/Declarative/MacroRules.lean
diff --git a/LeanByExample/Declarative/Namespace.lean → ...mple/Reference/Declarative/Namespace.lean b/LeanByExample/Declarative/Namespace.lean → ...mple/Reference/Declarative/Namespace.lean
diff --git a/LeanByExample/Declarative/Noncomputable.lean → .../Reference/Declarative/Noncomputable.lean b/LeanByExample/Declarative/Noncomputable.lean → .../Reference/Declarative/Noncomputable.lean
diff --git a/LeanByExample/Declarative/Notation.lean → ...ample/Reference/Declarative/Notation.lean b/LeanByExample/Declarative/Notation.lean → ...ample/Reference/Declarative/Notation.lean
diff --git a/LeanByExample/Declarative/Opaque.lean → ...Example/Reference/Declarative/Opaque.lean b/LeanByExample/Declarative/Opaque.lean → ...Example/Reference/Declarative/Opaque.lean
diff --git a/LeanByExample/Declarative/Open.lean → ...ByExample/Reference/Declarative/Open.lean b/LeanByExample/Declarative/Open.lean → ...ByExample/Reference/Declarative/Open.lean
diff --git a/LeanByExample/Declarative/Partial.lean → ...xample/Reference/Declarative/Partial.lean b/LeanByExample/Declarative/Partial.lean → ...xample/Reference/Declarative/Partial.lean
diff --git a/LeanByExample/Declarative/Postfix.lean → ...xample/Reference/Declarative/Postfix.lean b/LeanByExample/Declarative/Postfix.lean → ...xample/Reference/Declarative/Postfix.lean
diff --git a/LeanByExample/Declarative/Prefix.lean → ...Example/Reference/Declarative/Prefix.lean b/LeanByExample/Declarative/Prefix.lean → ...Example/Reference/Declarative/Prefix.lean
diff --git a/LeanByExample/Declarative/Private.lean → ...xample/Reference/Declarative/Private.lean b/LeanByExample/Declarative/Private.lean → ...xample/Reference/Declarative/Private.lean
@@ -3,7 +3,7 @@
 
 不安定なAPIなど、外部に公開したくないものに対して使うのが主な用途です。
 -/
-import Examples.Declarative.Protected -- protected のページをインポート
+import LeanByExample.Reference.Declarative.Protected -- protected のページをインポート
 import Lean
 namespace Private --#
 

diff --git a/LeanByExample/Declarative/ProofWanted.lean → ...le/Reference/Declarative/ProofWanted.lean b/LeanByExample/Declarative/ProofWanted.lean → ...le/Reference/Declarative/ProofWanted.lean
diff --git a/LeanByExample/Declarative/Protected.lean → ...mple/Reference/Declarative/Protected.lean b/LeanByExample/Declarative/Protected.lean → ...mple/Reference/Declarative/Protected.lean
diff --git a/LeanByExample/Declarative/README.lean → ...Example/Reference/Declarative/README.lean b/LeanByExample/Declarative/README.lean → ...Example/Reference/Declarative/README.lean
diff --git a/LeanByExample/Declarative/Scoped.lean → ...Example/Reference/Declarative/Scoped.lean b/LeanByExample/Declarative/Scoped.lean → ...Example/Reference/Declarative/Scoped.lean
diff --git a/LeanByExample/Declarative/Section.lean → ...xample/Reference/Declarative/Section.lean b/LeanByExample/Declarative/Section.lean → ...xample/Reference/Declarative/Section.lean
diff --git a/LeanByExample/Declarative/SetOption.lean → ...mple/Reference/Declarative/SetOption.lean b/LeanByExample/Declarative/SetOption.lean → ...mple/Reference/Declarative/SetOption.lean
diff --git a/LeanByExample/Declarative/Structure.lean → ...mple/Reference/Declarative/Structure.lean b/LeanByExample/Declarative/Structure.lean → ...mple/Reference/Declarative/Structure.lean
diff --git a/LeanByExample/Declarative/Syntax.lean → ...Example/Reference/Declarative/Syntax.lean b/LeanByExample/Declarative/Syntax.lean → ...Example/Reference/Declarative/Syntax.lean
diff --git a/LeanByExample/Declarative/TerminationBy.lean → .../Reference/Declarative/TerminationBy.lean b/LeanByExample/Declarative/TerminationBy.lean → .../Reference/Declarative/TerminationBy.lean
diff --git a/LeanByExample/Declarative/Theorem.lean → ...xample/Reference/Declarative/Theorem.lean b/LeanByExample/Declarative/Theorem.lean → ...xample/Reference/Declarative/Theorem.lean
diff --git a/LeanByExample/Declarative/Variable.lean → ...ample/Reference/Declarative/Variable.lean b/LeanByExample/Declarative/Variable.lean → ...ample/Reference/Declarative/Variable.lean
diff --git a/LeanByExample/Diagnostic/Check.lean → ...ByExample/Reference/Diagnostic/Check.lean b/LeanByExample/Diagnostic/Check.lean → ...ByExample/Reference/Diagnostic/Check.lean
diff --git a/LeanByExample/Diagnostic/CheckFailure.lean → ...le/Reference/Diagnostic/CheckFailure.lean b/LeanByExample/Diagnostic/CheckFailure.lean → ...le/Reference/Diagnostic/CheckFailure.lean
diff --git a/LeanByExample/Diagnostic/Eval.lean → LeanByExample/Reference/Diagnostic/Eval.lean b/LeanByExample/Diagnostic/Eval.lean → LeanByExample/Reference/Diagnostic/Eval.lean
diff --git a/LeanByExample/Diagnostic/Find.lean → LeanByExample/Reference/Diagnostic/Find.lean b/LeanByExample/Diagnostic/Find.lean → LeanByExample/Reference/Diagnostic/Find.lean
diff --git a/LeanByExample/Diagnostic/Guard.lean → ...ByExample/Reference/Diagnostic/Guard.lean b/LeanByExample/Diagnostic/Guard.lean → ...ByExample/Reference/Diagnostic/Guard.lean
diff --git a/LeanByExample/Diagnostic/GuardMsgs.lean → ...ample/Reference/Diagnostic/GuardMsgs.lean b/LeanByExample/Diagnostic/GuardMsgs.lean → ...ample/Reference/Diagnostic/GuardMsgs.lean
diff --git a/LeanByExample/Diagnostic/Help.lean → LeanByExample/Reference/Diagnostic/Help.lean b/LeanByExample/Diagnostic/Help.lean → LeanByExample/Reference/Diagnostic/Help.lean
diff --git a/LeanByExample/Diagnostic/Instances.lean → ...ample/Reference/Diagnostic/Instances.lean b/LeanByExample/Diagnostic/Instances.lean → ...ample/Reference/Diagnostic/Instances.lean
diff --git a/LeanByExample/Diagnostic/Print.lean → ...ByExample/Reference/Diagnostic/Print.lean b/LeanByExample/Diagnostic/Print.lean → ...ByExample/Reference/Diagnostic/Print.lean
diff --git a/LeanByExample/Diagnostic/README.lean → ...yExample/Reference/Diagnostic/README.lean b/LeanByExample/Diagnostic/README.lean → ...yExample/Reference/Diagnostic/README.lean
diff --git a/LeanByExample/Diagnostic/Reduce.lean → ...yExample/Reference/Diagnostic/Reduce.lean b/LeanByExample/Diagnostic/Reduce.lean → ...yExample/Reference/Diagnostic/Reduce.lean
diff --git a/LeanByExample/Diagnostic/Synth.lean → ...ByExample/Reference/Diagnostic/Synth.lean b/LeanByExample/Diagnostic/Synth.lean → ...ByExample/Reference/Diagnostic/Synth.lean
diff --git a/LeanByExample/Diagnostic/Time.lean → LeanByExample/Reference/Diagnostic/Time.lean b/LeanByExample/Diagnostic/Time.lean → LeanByExample/Reference/Diagnostic/Time.lean
diff --git a/LeanByExample/Diagnostic/Whnf.lean → LeanByExample/Reference/Diagnostic/Whnf.lean b/LeanByExample/Diagnostic/Whnf.lean → LeanByExample/Reference/Diagnostic/Whnf.lean
diff --git a/LeanByExample/Option/AutoImplicit.lean → ...xample/Reference/Option/AutoImplicit.lean b/LeanByExample/Option/AutoImplicit.lean → ...xample/Reference/Option/AutoImplicit.lean
diff --git a/LeanByExample/Option/Flexible.lean → LeanByExample/Reference/Option/Flexible.lean b/LeanByExample/Option/Flexible.lean → LeanByExample/Reference/Option/Flexible.lean
diff --git a/LeanByExample/Option/Hygiene.lean → LeanByExample/Reference/Option/Hygiene.lean b/LeanByExample/Option/Hygiene.lean → LeanByExample/Reference/Option/Hygiene.lean
diff --git a/LeanByExample/Option/README.lean → LeanByExample/Reference/Option/README.lean b/LeanByExample/Option/README.lean → LeanByExample/Reference/Option/README.lean
diff --git a/LeanByExample/Tactic/AcRfl.lean → LeanByExample/Reference/Tactic/AcRfl.lean b/LeanByExample/Tactic/AcRfl.lean → LeanByExample/Reference/Tactic/AcRfl.lean
diff --git a/LeanByExample/Tactic/Aesop.lean → LeanByExample/Reference/Tactic/Aesop.lean b/LeanByExample/Tactic/Aesop.lean → LeanByExample/Reference/Tactic/Aesop.lean
diff --git a/LeanByExample/Tactic/AllGoals.lean → LeanByExample/Reference/Tactic/AllGoals.lean b/LeanByExample/Tactic/AllGoals.lean → LeanByExample/Reference/Tactic/AllGoals.lean
diff --git a/LeanByExample/Tactic/Apply.lean → LeanByExample/Reference/Tactic/Apply.lean b/LeanByExample/Tactic/Apply.lean → LeanByExample/Reference/Tactic/Apply.lean
diff --git a/LeanByExample/Tactic/ApplyAssumption.lean → ...ple/Reference/Tactic/ApplyAssumption.lean b/LeanByExample/Tactic/ApplyAssumption.lean → ...ple/Reference/Tactic/ApplyAssumption.lean
diff --git a/LeanByExample/Tactic/ApplyAt.lean → LeanByExample/Reference/Tactic/ApplyAt.lean b/LeanByExample/Tactic/ApplyAt.lean → LeanByExample/Reference/Tactic/ApplyAt.lean
diff --git a/LeanByExample/Tactic/ApplyQuestion.lean → ...ample/Reference/Tactic/ApplyQuestion.lean b/LeanByExample/Tactic/ApplyQuestion.lean → ...ample/Reference/Tactic/ApplyQuestion.lean
diff --git a/LeanByExample/Tactic/Assumption.lean → ...yExample/Reference/Tactic/Assumption.lean b/LeanByExample/Tactic/Assumption.lean → ...yExample/Reference/Tactic/Assumption.lean
diff --git a/LeanByExample/Tactic/By.lean → LeanByExample/Reference/Tactic/By.lean b/LeanByExample/Tactic/By.lean → LeanByExample/Reference/Tactic/By.lean
diff --git a/LeanByExample/Tactic/ByCases.lean → LeanByExample/Reference/Tactic/ByCases.lean b/LeanByExample/Tactic/ByCases.lean → LeanByExample/Reference/Tactic/ByCases.lean
diff --git a/LeanByExample/Tactic/ByContra.lean → LeanByExample/Reference/Tactic/ByContra.lean b/LeanByExample/Tactic/ByContra.lean → LeanByExample/Reference/Tactic/ByContra.lean
diff --git a/LeanByExample/Tactic/Calc.lean → LeanByExample/Reference/Tactic/Calc.lean b/LeanByExample/Tactic/Calc.lean → LeanByExample/Reference/Tactic/Calc.lean
diff --git a/LeanByExample/Tactic/Cases.lean → LeanByExample/Reference/Tactic/Cases.lean b/LeanByExample/Tactic/Cases.lean → LeanByExample/Reference/Tactic/Cases.lean
diff --git a/LeanByExample/Tactic/CasesAp.lean → LeanByExample/Reference/Tactic/CasesAp.lean b/LeanByExample/Tactic/CasesAp.lean → LeanByExample/Reference/Tactic/CasesAp.lean
diff --git a/LeanByExample/Tactic/Choose.lean → LeanByExample/Reference/Tactic/Choose.lean b/LeanByExample/Tactic/Choose.lean → LeanByExample/Reference/Tactic/Choose.lean
diff --git a/LeanByExample/Tactic/Clear.lean → LeanByExample/Reference/Tactic/Clear.lean b/LeanByExample/Tactic/Clear.lean → LeanByExample/Reference/Tactic/Clear.lean
diff --git a/LeanByExample/Tactic/Congr.lean → LeanByExample/Reference/Tactic/Congr.lean b/LeanByExample/Tactic/Congr.lean → LeanByExample/Reference/Tactic/Congr.lean
diff --git a/LeanByExample/Tactic/Constructor.lean → ...Example/Reference/Tactic/Constructor.lean b/LeanByExample/Tactic/Constructor.lean → ...Example/Reference/Tactic/Constructor.lean
diff --git a/LeanByExample/Tactic/Contradiction.lean → ...ample/Reference/Tactic/Contradiction.lean b/LeanByExample/Tactic/Contradiction.lean → ...ample/Reference/Tactic/Contradiction.lean
diff --git a/LeanByExample/Tactic/Contrapose.lean → ...yExample/Reference/Tactic/Contrapose.lean b/LeanByExample/Tactic/Contrapose.lean → ...yExample/Reference/Tactic/Contrapose.lean
diff --git a/LeanByExample/Tactic/Conv.lean → LeanByExample/Reference/Tactic/Conv.lean b/LeanByExample/Tactic/Conv.lean → LeanByExample/Reference/Tactic/Conv.lean
diff --git a/LeanByExample/Tactic/Convert.lean → LeanByExample/Reference/Tactic/Convert.lean b/LeanByExample/Tactic/Convert.lean → LeanByExample/Reference/Tactic/Convert.lean
diff --git a/LeanByExample/Tactic/Decide.lean → LeanByExample/Reference/Tactic/Decide.lean b/LeanByExample/Tactic/Decide.lean → LeanByExample/Reference/Tactic/Decide.lean
diff --git a/LeanByExample/Tactic/Done.lean → LeanByExample/Reference/Tactic/Done.lean b/LeanByExample/Tactic/Done.lean → LeanByExample/Reference/Tactic/Done.lean
diff --git a/LeanByExample/Tactic/Dsimp.lean → LeanByExample/Reference/Tactic/Dsimp.lean b/LeanByExample/Tactic/Dsimp.lean → LeanByExample/Reference/Tactic/Dsimp.lean
diff --git a/LeanByExample/Tactic/Exact.lean → LeanByExample/Reference/Tactic/Exact.lean b/LeanByExample/Tactic/Exact.lean → LeanByExample/Reference/Tactic/Exact.lean
diff --git a/LeanByExample/Tactic/ExactQuestion.lean → ...ample/Reference/Tactic/ExactQuestion.lean b/LeanByExample/Tactic/ExactQuestion.lean → ...ample/Reference/Tactic/ExactQuestion.lean
diff --git a/LeanByExample/Tactic/Exfalso.lean → LeanByExample/Reference/Tactic/Exfalso.lean b/LeanByExample/Tactic/Exfalso.lean → LeanByExample/Reference/Tactic/Exfalso.lean
diff --git a/LeanByExample/Tactic/Exists.lean → LeanByExample/Reference/Tactic/Exists.lean b/LeanByExample/Tactic/Exists.lean → LeanByExample/Reference/Tactic/Exists.lean
diff --git a/LeanByExample/Tactic/Ext.lean → LeanByExample/Reference/Tactic/Ext.lean b/LeanByExample/Tactic/Ext.lean → LeanByExample/Reference/Tactic/Ext.lean
diff --git a/LeanByExample/Tactic/FieldSimp.lean → ...ByExample/Reference/Tactic/FieldSimp.lean b/LeanByExample/Tactic/FieldSimp.lean → ...ByExample/Reference/Tactic/FieldSimp.lean
diff --git a/LeanByExample/Tactic/FinCases.lean → LeanByExample/Reference/Tactic/FinCases.lean b/LeanByExample/Tactic/FinCases.lean → LeanByExample/Reference/Tactic/FinCases.lean
diff --git a/LeanByExample/Tactic/FunProp.lean → LeanByExample/Reference/Tactic/FunProp.lean b/LeanByExample/Tactic/FunProp.lean → LeanByExample/Reference/Tactic/FunProp.lean
diff --git a/LeanByExample/Tactic/Funext.lean → LeanByExample/Reference/Tactic/Funext.lean b/LeanByExample/Tactic/Funext.lean → LeanByExample/Reference/Tactic/Funext.lean
diff --git a/LeanByExample/Tactic/Gcongr.lean → LeanByExample/Reference/Tactic/Gcongr.lean b/LeanByExample/Tactic/Gcongr.lean → LeanByExample/Reference/Tactic/Gcongr.lean
diff --git a/LeanByExample/Tactic/Generalize.lean → ...yExample/Reference/Tactic/Generalize.lean b/LeanByExample/Tactic/Generalize.lean → ...yExample/Reference/Tactic/Generalize.lean
diff --git a/LeanByExample/Tactic/GuardHyp.lean → LeanByExample/Reference/Tactic/GuardHyp.lean b/LeanByExample/Tactic/GuardHyp.lean → LeanByExample/Reference/Tactic/GuardHyp.lean
diff --git a/LeanByExample/Tactic/Have.lean → LeanByExample/Reference/Tactic/Have.lean b/LeanByExample/Tactic/Have.lean → LeanByExample/Reference/Tactic/Have.lean
diff --git a/LeanByExample/Tactic/Hint.lean → LeanByExample/Reference/Tactic/Hint.lean b/LeanByExample/Tactic/Hint.lean → LeanByExample/Reference/Tactic/Hint.lean
diff --git a/LeanByExample/Tactic/Induction.lean → ...ByExample/Reference/Tactic/Induction.lean b/LeanByExample/Tactic/Induction.lean → ...ByExample/Reference/Tactic/Induction.lean
diff --git a/LeanByExample/Tactic/InductionAp.lean → ...Example/Reference/Tactic/InductionAp.lean b/LeanByExample/Tactic/InductionAp.lean → ...Example/Reference/Tactic/InductionAp.lean
diff --git a/LeanByExample/Tactic/Intro.lean → LeanByExample/Reference/Tactic/Intro.lean b/LeanByExample/Tactic/Intro.lean → LeanByExample/Reference/Tactic/Intro.lean
diff --git a/LeanByExample/Tactic/Itauto.lean → LeanByExample/Reference/Tactic/Itauto.lean b/LeanByExample/Tactic/Itauto.lean → LeanByExample/Reference/Tactic/Itauto.lean
diff --git a/LeanByExample/Tactic/Left.lean → LeanByExample/Reference/Tactic/Left.lean b/LeanByExample/Tactic/Left.lean → LeanByExample/Reference/Tactic/Left.lean
diff --git a/LeanByExample/Tactic/Linarith.lean → LeanByExample/Reference/Tactic/Linarith.lean b/LeanByExample/Tactic/Linarith.lean → LeanByExample/Reference/Tactic/Linarith.lean
diff --git a/LeanByExample/Tactic/NativeDecide.lean → ...xample/Reference/Tactic/NativeDecide.lean b/LeanByExample/Tactic/NativeDecide.lean → ...xample/Reference/Tactic/NativeDecide.lean
diff --git a/LeanByExample/Tactic/Nlinarith.lean → ...ByExample/Reference/Tactic/Nlinarith.lean b/LeanByExample/Tactic/Nlinarith.lean → ...ByExample/Reference/Tactic/Nlinarith.lean
diff --git a/LeanByExample/Tactic/NormCast.lean → LeanByExample/Reference/Tactic/NormCast.lean b/LeanByExample/Tactic/NormCast.lean → LeanByExample/Reference/Tactic/NormCast.lean
diff --git a/LeanByExample/Tactic/NthRw.lean → LeanByExample/Reference/Tactic/NthRw.lean b/LeanByExample/Tactic/NthRw.lean → LeanByExample/Reference/Tactic/NthRw.lean
diff --git a/LeanByExample/Tactic/Obtain.lean → LeanByExample/Reference/Tactic/Obtain.lean b/LeanByExample/Tactic/Obtain.lean → LeanByExample/Reference/Tactic/Obtain.lean
diff --git a/LeanByExample/Tactic/Omega.lean → LeanByExample/Reference/Tactic/Omega.lean b/LeanByExample/Tactic/Omega.lean → LeanByExample/Reference/Tactic/Omega.lean
diff --git a/LeanByExample/Tactic/Positivity.lean → ...yExample/Reference/Tactic/Positivity.lean b/LeanByExample/Tactic/Positivity.lean → ...yExample/Reference/Tactic/Positivity.lean
diff --git a/LeanByExample/Tactic/PushNeg.lean → LeanByExample/Reference/Tactic/PushNeg.lean b/LeanByExample/Tactic/PushNeg.lean → LeanByExample/Reference/Tactic/PushNeg.lean
diff --git a/LeanByExample/Tactic/Qify.lean → LeanByExample/Reference/Tactic/Qify.lean b/LeanByExample/Tactic/Qify.lean → LeanByExample/Reference/Tactic/Qify.lean
diff --git a/LeanByExample/Tactic/README.lean → LeanByExample/Reference/Tactic/README.lean b/LeanByExample/Tactic/README.lean → LeanByExample/Reference/Tactic/README.lean
diff --git a/LeanByExample/Tactic/Rcases.lean → LeanByExample/Reference/Tactic/Rcases.lean b/LeanByExample/Tactic/Rcases.lean → LeanByExample/Reference/Tactic/Rcases.lean
diff --git a/LeanByExample/Tactic/Refine.lean → LeanByExample/Reference/Tactic/Refine.lean b/LeanByExample/Tactic/Refine.lean → LeanByExample/Reference/Tactic/Refine.lean
diff --git a/LeanByExample/Tactic/Rel.lean → LeanByExample/Reference/Tactic/Rel.lean b/LeanByExample/Tactic/Rel.lean → LeanByExample/Reference/Tactic/Rel.lean
diff --git a/LeanByExample/Tactic/RenameI.lean → LeanByExample/Reference/Tactic/RenameI.lean b/LeanByExample/Tactic/RenameI.lean → LeanByExample/Reference/Tactic/RenameI.lean
diff --git a/LeanByExample/Tactic/Repeat.lean → LeanByExample/Reference/Tactic/Repeat.lean b/LeanByExample/Tactic/Repeat.lean → LeanByExample/Reference/Tactic/Repeat.lean
diff --git a/LeanByExample/Tactic/Replace.lean → LeanByExample/Reference/Tactic/Replace.lean b/LeanByExample/Tactic/Replace.lean → LeanByExample/Reference/Tactic/Replace.lean
diff --git a/LeanByExample/Tactic/Rfl.lean → LeanByExample/Reference/Tactic/Rfl.lean b/LeanByExample/Tactic/Rfl.lean → LeanByExample/Reference/Tactic/Rfl.lean
diff --git a/LeanByExample/Tactic/Right.lean → LeanByExample/Reference/Tactic/Right.lean b/LeanByExample/Tactic/Right.lean → LeanByExample/Reference/Tactic/Right.lean
diff --git a/LeanByExample/Tactic/Ring.lean → LeanByExample/Reference/Tactic/Ring.lean b/LeanByExample/Tactic/Ring.lean → LeanByExample/Reference/Tactic/Ring.lean
diff --git a/LeanByExample/Tactic/Rw.lean → LeanByExample/Reference/Tactic/Rw.lean b/LeanByExample/Tactic/Rw.lean → LeanByExample/Reference/Tactic/Rw.lean
diff --git a/LeanByExample/Tactic/RwSearch.lean → LeanByExample/Reference/Tactic/RwSearch.lean b/LeanByExample/Tactic/RwSearch.lean → LeanByExample/Reference/Tactic/RwSearch.lean
diff --git a/LeanByExample/Tactic/Says.lean → LeanByExample/Reference/Tactic/Says.lean b/LeanByExample/Tactic/Says.lean → LeanByExample/Reference/Tactic/Says.lean
diff --git a/LeanByExample/Tactic/SeqFocus.lean → LeanByExample/Reference/Tactic/SeqFocus.lean b/LeanByExample/Tactic/SeqFocus.lean → LeanByExample/Reference/Tactic/SeqFocus.lean
diff --git a/LeanByExample/Tactic/Set.lean → LeanByExample/Reference/Tactic/Set.lean b/LeanByExample/Tactic/Set.lean → LeanByExample/Reference/Tactic/Set.lean
diff --git a/LeanByExample/Tactic/Show.lean → LeanByExample/Reference/Tactic/Show.lean b/LeanByExample/Tactic/Show.lean → LeanByExample/Reference/Tactic/Show.lean
diff --git a/LeanByExample/Tactic/Simp.lean → LeanByExample/Reference/Tactic/Simp.lean b/LeanByExample/Tactic/Simp.lean → LeanByExample/Reference/Tactic/Simp.lean
diff --git a/LeanByExample/Tactic/SlimCheck.lean → ...ByExample/Reference/Tactic/SlimCheck.lean b/LeanByExample/Tactic/SlimCheck.lean → ...ByExample/Reference/Tactic/SlimCheck.lean
diff --git a/LeanByExample/Tactic/Sorry.lean → LeanByExample/Reference/Tactic/Sorry.lean b/LeanByExample/Tactic/Sorry.lean → LeanByExample/Reference/Tactic/Sorry.lean
diff --git a/LeanByExample/Tactic/Split.lean → LeanByExample/Reference/Tactic/Split.lean b/LeanByExample/Tactic/Split.lean → LeanByExample/Reference/Tactic/Split.lean
diff --git a/LeanByExample/Tactic/Suffices.lean → LeanByExample/Reference/Tactic/Suffices.lean b/LeanByExample/Tactic/Suffices.lean → LeanByExample/Reference/Tactic/Suffices.lean
diff --git a/LeanByExample/Tactic/Tauto.lean → LeanByExample/Reference/Tactic/Tauto.lean b/LeanByExample/Tactic/Tauto.lean → LeanByExample/Reference/Tactic/Tauto.lean
diff --git a/LeanByExample/Tactic/Trans.lean → LeanByExample/Reference/Tactic/Trans.lean b/LeanByExample/Tactic/Trans.lean → LeanByExample/Reference/Tactic/Trans.lean
diff --git a/LeanByExample/Tactic/Trivial.lean → LeanByExample/Reference/Tactic/Trivial.lean b/LeanByExample/Tactic/Trivial.lean → LeanByExample/Reference/Tactic/Trivial.lean
diff --git a/LeanByExample/Tactic/Try.lean → LeanByExample/Reference/Tactic/Try.lean b/LeanByExample/Tactic/Try.lean → LeanByExample/Reference/Tactic/Try.lean
diff --git a/LeanByExample/Tactic/Unfold.lean → LeanByExample/Reference/Tactic/Unfold.lean b/LeanByExample/Tactic/Unfold.lean → LeanByExample/Reference/Tactic/Unfold.lean
diff --git a/LeanByExample/Tactic/WithReducible.lean → ...ample/Reference/Tactic/WithReducible.lean b/LeanByExample/Tactic/WithReducible.lean → ...ample/Reference/Tactic/WithReducible.lean
diff --git a/LeanByExample/Tactic/Wlog.lean → LeanByExample/Reference/Tactic/Wlog.lean b/LeanByExample/Tactic/Wlog.lean → LeanByExample/Reference/Tactic/Wlog.lean
diff --git a/LeanByExample/Type/Char.lean → LeanByExample/Reference/Type/Char.lean b/LeanByExample/Type/Char.lean → LeanByExample/Reference/Type/Char.lean
diff --git a/LeanByExample/Type/Float.lean → LeanByExample/Reference/Type/Float.lean b/LeanByExample/Type/Float.lean → LeanByExample/Reference/Type/Float.lean
diff --git a/LeanByExample/Type/List.lean → LeanByExample/Reference/Type/List.lean b/LeanByExample/Type/List.lean → LeanByExample/Reference/Type/List.lean
diff --git a/LeanByExample/Type/Prop.lean → LeanByExample/Reference/Type/Prop.lean b/LeanByExample/Type/Prop.lean → LeanByExample/Reference/Type/Prop.lean
diff --git a/LeanByExample/Type/README.lean → LeanByExample/Reference/Type/README.lean b/LeanByExample/Type/README.lean → LeanByExample/Reference/Type/README.lean
diff --git a/LeanByExample/Type/String.lean → LeanByExample/Reference/Type/String.lean b/LeanByExample/Type/String.lean → LeanByExample/Reference/Type/String.lean
diff --git a/LeanByExample/Type/Type.lean → LeanByExample/Reference/Type/Type.lean b/LeanByExample/Type/Type.lean → LeanByExample/Reference/Type/Type.lean
diff --git a/LeanByExample/TypeClass/Coe.lean → LeanByExample/Reference/TypeClass/Coe.lean b/LeanByExample/TypeClass/Coe.lean → LeanByExample/Reference/TypeClass/Coe.lean
diff --git a/LeanByExample/TypeClass/CoeDep.lean → ...ByExample/Reference/TypeClass/CoeDep.lean b/LeanByExample/TypeClass/CoeDep.lean → ...ByExample/Reference/TypeClass/CoeDep.lean
diff --git a/LeanByExample/TypeClass/CoeFun.lean → ...ByExample/Reference/TypeClass/CoeFun.lean b/LeanByExample/TypeClass/CoeFun.lean → ...ByExample/Reference/TypeClass/CoeFun.lean
diff --git a/LeanByExample/TypeClass/CoeSort.lean → ...yExample/Reference/TypeClass/CoeSort.lean b/LeanByExample/TypeClass/CoeSort.lean → ...yExample/Reference/TypeClass/CoeSort.lean
diff --git a/LeanByExample/TypeClass/Decidable.lean → ...xample/Reference/TypeClass/Decidable.lean b/LeanByExample/TypeClass/Decidable.lean → ...xample/Reference/TypeClass/Decidable.lean
diff --git a/LeanByExample/TypeClass/GetElem.lean → ...yExample/Reference/TypeClass/GetElem.lean b/LeanByExample/TypeClass/GetElem.lean → ...yExample/Reference/TypeClass/GetElem.lean
diff --git a/LeanByExample/TypeClass/Inhabited.lean → ...xample/Reference/TypeClass/Inhabited.lean b/LeanByExample/TypeClass/Inhabited.lean → ...xample/Reference/TypeClass/Inhabited.lean
diff --git a/LeanByExample/TypeClass/OfNat.lean → LeanByExample/Reference/TypeClass/OfNat.lean b/LeanByExample/TypeClass/OfNat.lean → LeanByExample/Reference/TypeClass/OfNat.lean
diff --git a/LeanByExample/TypeClass/README.lean → ...ByExample/Reference/TypeClass/README.lean b/LeanByExample/TypeClass/README.lean → ...ByExample/Reference/TypeClass/README.lean
diff --git a/LeanByExample/TypeClass/Repr.lean → LeanByExample/Reference/TypeClass/Repr.lean b/LeanByExample/TypeClass/Repr.lean → LeanByExample/Reference/TypeClass/Repr.lean
diff --git a/LeanByExample/TypeClass/ToString.lean → ...Example/Reference/TypeClass/ToString.lean b/LeanByExample/TypeClass/ToString.lean → ...Example/Reference/TypeClass/ToString.lean
diff --git a/Exercise/BarberParadox.lean → ...mple/Tutorial/Exercise/BarberParadox.lean b/Exercise/BarberParadox.lean → ...mple/Tutorial/Exercise/BarberParadox.lean
diff --git a/Exercise/CantorPairing.lean → ...mple/Tutorial/Exercise/CantorPairing.lean b/Exercise/CantorPairing.lean → ...mple/Tutorial/Exercise/CantorPairing.lean
diff --git a/Exercise/CantorTheorem.lean → ...mple/Tutorial/Exercise/CantorTheorem.lean b/Exercise/CantorTheorem.lean → ...mple/Tutorial/Exercise/CantorTheorem.lean
diff --git a/Exercise/DoubtImplication.lean → ...e/Tutorial/Exercise/DoubtImplication.lean b/Exercise/DoubtImplication.lean → ...e/Tutorial/Exercise/DoubtImplication.lean
diff --git a/Exercise/HeytingAndBooleanAlgebra.lean → ...al/Exercise/HeytingAndBooleanAlgebra.lean b/Exercise/HeytingAndBooleanAlgebra.lean → ...al/Exercise/HeytingAndBooleanAlgebra.lean
@@ -136,7 +136,7 @@ end HeytingAlgebra
 
 しかし、今回は証明の `sorry` の部分を埋めていただくという問題ではありません。逆に、こちらで用意した証明が通るようにしていただくのが問題です。
 
-こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](../Declarative/AddAesopRules.md) の記事が参考になると思います。
+こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](#{root}/Reference/Declarative/AddAesopRules.md) の記事が参考になると思います。
 
 ### 問1.1 半順序集合であること
 -/

diff --git a/Exercise/InverseSurjInj.lean → ...ple/Tutorial/Exercise/InverseSurjInj.lean b/Exercise/InverseSurjInj.lean → ...ple/Tutorial/Exercise/InverseSurjInj.lean
@@ -17,7 +17,7 @@ def Function.Injective (f : A → B) : Prop := ∀ {a₁ a₂ : A}, f a₁ = f a
 
 /- 一見すると、全射と単射はペアになる概念とは思えないかもしれません。束縛変数の数も違いますし、意味上もまったく独立した概念のように見えます。
 
-しかし、`A` が空でないと仮定すれば、選択原理 [`Classical.choice`](../Declarative/Axiom.md#ClassicalChoice) を使うことによって、全射 `f : A → B` があれば逆方向の単射 `g : B → A` が構成でき、逆に単射 `f : A → B` があれば逆方向の全射 `g : B → A` を構成することができます。
+しかし、`A` が空でないと仮定すれば、選択原理 [`Classical.choice`](#{root}/Reference/Declarative/Axiom.md#ClassicalChoice) を使うことによって、全射 `f : A → B` があれば逆方向の単射 `g : B → A` が構成でき、逆に単射 `f : A → B` があれば逆方向の全射 `g : B → A` を構成することができます。
 
 ある意味で、全射と単射はペアをなす概念であると言えるかもしれないですね。今回の演習問題のテーマはこの定理です。
 -/

diff --git a/Exercise/KnightAndKnave.lean → ...ple/Tutorial/Exercise/KnightAndKnave.lean b/Exercise/KnightAndKnave.lean → ...ple/Tutorial/Exercise/KnightAndKnave.lean
diff --git a/LeanByExample/Solution/README.lean → LeanByExample/Tutorial/Exercise/README.lean b/LeanByExample/Solution/README.lean → LeanByExample/Tutorial/Exercise/README.lean
@@ -7,13 +7,13 @@
 
 解き始めるための最も簡単で手軽な方法は、Lean 4 Playground を使う方法です。各ページの右上に <i class="fa fa-play"></i> というボタンがあるので、これをクリックしてください。Lean 4 Playground のページに移動し、そのままブラウザ上で演習問題を解き始めることができます。
 
-Lean 4 Playground を使いたくない事情がある場合は、Codespace を開き、`Exercise` ディレクトリの中にある該当ファイルを開いてください。
+Lean 4 Playground を使いたくない事情がある場合は、Codespace を開き、`LeanByExample/Tutorial/Exercise` ディレクトリの中にある該当ファイルを開いてください。
 
 [![codespace badge](https://github.com/codespaces/badge.svg)](https://codespaces.new/lean-ja/lean-by-example)
 
 ## ❓ どうしてもわからないとき
 
 時間をかけて考えてみてください。著者は簡単な問題をたくさん解くのではなく、おもしろい問題にじっくり取り組んだ方が学びは大きいと信じています。どの問題も、本書のレファレンス部分を参照しつつ試行錯誤をすれば自力で解けることを目指して作っています。
 
-しかし、自力で解いた後に解答を見るのは構いません。解答は [`Examples/Solution`](https://github.com/lean-ja/lean-by-example/tree/main/Examples/Solution) ディレクトリに置いてあります。
+しかし、自力で解いた後に解答を見るのは構いません。解答は `LeanByExample/Tutorial/Solution` ディレクトリに置いてあります。
 -/
diff --git a/LeanByExample/Solution/BarberParadox.lean → ...mple/Tutorial/Solution/BarberParadox.lean b/LeanByExample/Solution/BarberParadox.lean → ...mple/Tutorial/Solution/BarberParadox.lean
diff --git a/LeanByExample/Solution/CantorPairing.lean → ...mple/Tutorial/Solution/CantorPairing.lean b/LeanByExample/Solution/CantorPairing.lean → ...mple/Tutorial/Solution/CantorPairing.lean
diff --git a/LeanByExample/Solution/CantorTheorem.lean → ...mple/Tutorial/Solution/CantorTheorem.lean b/LeanByExample/Solution/CantorTheorem.lean → ...mple/Tutorial/Solution/CantorTheorem.lean
diff --git a/LeanByExample/Solution/DoubtImplication.lean → ...e/Tutorial/Solution/DoubtImplication.lean b/LeanByExample/Solution/DoubtImplication.lean → ...e/Tutorial/Solution/DoubtImplication.lean
diff --git a/...le/Solution/HeytingAndBooleanAlgebra.lean → ...al/Solution/HeytingAndBooleanAlgebra.lean b/...le/Solution/HeytingAndBooleanAlgebra.lean → ...al/Solution/HeytingAndBooleanAlgebra.lean
@@ -136,7 +136,7 @@ end HeytingAlgebra
 
 しかし、今回は証明の `sorry` の部分を埋めていただくという問題ではありません。逆に、こちらで用意した証明が通るようにしていただくのが問題です。
 
-こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](../Declarative/AddAesopRules.md) の記事が参考になると思います。
+こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](#{root}/Reference/Declarative/AddAesopRules.md) の記事が参考になると思います。
 
 ### 問1.1 半順序集合であること
 -/

diff --git a/LeanByExample/Solution/InverseSurjInj.lean → ...ple/Tutorial/Solution/InverseSurjInj.lean b/LeanByExample/Solution/InverseSurjInj.lean → ...ple/Tutorial/Solution/InverseSurjInj.lean
@@ -17,7 +17,7 @@ def Function.Injective (f : A → B) : Prop := ∀ {a₁ a₂ : A}, f a₁ = f a
 
 /- 一見すると、全射と単射はペアになる概念とは思えないかもしれません。束縛変数の数も違いますし、意味上もまったく独立した概念のように見えます。
 
-しかし、`A` が空でないと仮定すれば、選択原理 [`Classical.choice`](../Declarative/Axiom.md#ClassicalChoice) を使うことによって、全射 `f : A → B` があれば逆方向の単射 `g : B → A` が構成でき、逆に単射 `f : A → B` があれば逆方向の全射 `g : B → A` を構成することができます。
+しかし、`A` が空でないと仮定すれば、選択原理 [`Classical.choice`](#{root}/Reference/Declarative/Axiom.md#ClassicalChoice) を使うことによって、全射 `f : A → B` があれば逆方向の単射 `g : B → A` が構成でき、逆に単射 `f : A → B` があれば逆方向の全射 `g : B → A` を構成することができます。
 
 ある意味で、全射と単射はペアをなす概念であると言えるかもしれないですね。今回の演習問題のテーマはこの定理です。
 -/

diff --git a/LeanByExample/Solution/KnightAndKnave.lean → ...ple/Tutorial/Solution/KnightAndKnave.lean b/LeanByExample/Solution/KnightAndKnave.lean → ...ple/Tutorial/Solution/KnightAndKnave.lean
diff --git a/Exercise/README.lean → LeanByExample/Tutorial/Solution/README.lean b/Exercise/README.lean → LeanByExample/Tutorial/Solution/README.lean
@@ -7,13 +7,13 @@
 
 解き始めるための最も簡単で手軽な方法は、Lean 4 Playground を使う方法です。各ページの右上に <i class="fa fa-play"></i> というボタンがあるので、これをクリックしてください。Lean 4 Playground のページに移動し、そのままブラウザ上で演習問題を解き始めることができます。
 
-Lean 4 Playground を使いたくない事情がある場合は、Codespace を開き、`Exercise` ディレクトリの中にある該当ファイルを開いてください。
+Lean 4 Playground を使いたくない事情がある場合は、Codespace を開き、`LeanByExample/Tutorial/Exercise` ディレクトリの中にある該当ファイルを開いてください。
 
 [![codespace badge](https://github.com/codespaces/badge.svg)](https://codespaces.new/lean-ja/lean-by-example)
 
 ## ❓ どうしてもわからないとき
 
 時間をかけて考えてみてください。著者は簡単な問題をたくさん解くのではなく、おもしろい問題にじっくり取り組んだ方が学びは大きいと信じています。どの問題も、本書のレファレンス部分を参照しつつ試行錯誤をすれば自力で解けることを目指して作っています。
 
-しかし、自力で解いた後に解答を見るのは構いません。解答は [`Examples/Solution`](https://github.com/lean-ja/lean-by-example/tree/main/Examples/Solution) ディレクトリに置いてあります。
+しかし、自力で解いた後に解答を見るのは構いません。解答は `LeanByExample/Tutorial/Solution` ディレクトリに置いてあります。
 -/
diff --git a/assets/filePlay.js b/assets/filePlay.js
@@ -20,12 +20,6 @@ function filePlay() {
     "/LeanByExample/",
   );
 
-  // 演習問題のファイルのみ、`LeanByExample` ディレクトリではなくて `Exercise` ディレクトリにある
-  editButtonLink.href = editButtonLink.href.replace(
-    "/LeanByExample/Exercise/",
-    "/Exercise/",
-  );
-
   // URL を書き換える
   fetch(editButtonLink.href)
     .then((response) => response.text())