diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index 0d274cb0..fac39544 100644 --- 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 index 28aa848e..c3f746eb 100644 --- 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 b/LeanByExample/Attribute/AppUnexpander.lean similarity index 100% rename from Examples/Attribute/AppUnexpander.lean rename to LeanByExample/Attribute/AppUnexpander.lean diff --git a/Examples/Attribute/CasesEliminator.lean b/LeanByExample/Attribute/CasesEliminator.lean similarity index 100% rename from Examples/Attribute/CasesEliminator.lean rename to LeanByExample/Attribute/CasesEliminator.lean diff --git a/Examples/Attribute/Coe.lean b/LeanByExample/Attribute/Coe.lean similarity index 100% rename from Examples/Attribute/Coe.lean rename to LeanByExample/Attribute/Coe.lean diff --git a/Examples/Attribute/Csimp.lean b/LeanByExample/Attribute/Csimp.lean similarity index 100% rename from Examples/Attribute/Csimp.lean rename to LeanByExample/Attribute/Csimp.lean diff --git a/Examples/Attribute/DefaultInstance.lean b/LeanByExample/Attribute/DefaultInstance.lean similarity index 100% rename from Examples/Attribute/DefaultInstance.lean rename to LeanByExample/Attribute/DefaultInstance.lean diff --git a/Examples/Attribute/InductionEliminator.lean b/LeanByExample/Attribute/InductionEliminator.lean similarity index 100% rename from Examples/Attribute/InductionEliminator.lean rename to LeanByExample/Attribute/InductionEliminator.lean diff --git a/Examples/Attribute/InheritDoc.lean b/LeanByExample/Attribute/InheritDoc.lean similarity index 100% rename from Examples/Attribute/InheritDoc.lean rename to LeanByExample/Attribute/InheritDoc.lean diff --git a/Examples/Attribute/MatchPattern.lean b/LeanByExample/Attribute/MatchPattern.lean similarity index 100% rename from Examples/Attribute/MatchPattern.lean rename to LeanByExample/Attribute/MatchPattern.lean diff --git a/Examples/Attribute/README.lean b/LeanByExample/Attribute/README.lean similarity index 100% rename from Examples/Attribute/README.lean rename to LeanByExample/Attribute/README.lean diff --git a/Examples/Attribute/Simps.lean b/LeanByExample/Attribute/Simps.lean similarity index 100% rename from Examples/Attribute/Simps.lean rename to LeanByExample/Attribute/Simps.lean diff --git a/Examples/Declarative/Abbrev.lean b/LeanByExample/Declarative/Abbrev.lean similarity index 100% rename from Examples/Declarative/Abbrev.lean rename to LeanByExample/Declarative/Abbrev.lean diff --git a/Examples/Declarative/AddAesopRules.lean b/LeanByExample/Declarative/AddAesopRules.lean similarity index 100% rename from Examples/Declarative/AddAesopRules.lean rename to LeanByExample/Declarative/AddAesopRules.lean diff --git a/Examples/Declarative/Attribute.lean b/LeanByExample/Declarative/Attribute.lean similarity index 100% rename from Examples/Declarative/Attribute.lean rename to LeanByExample/Declarative/Attribute.lean diff --git a/Examples/Declarative/Axiom.lean b/LeanByExample/Declarative/Axiom.lean similarity index 100% rename from Examples/Declarative/Axiom.lean rename to LeanByExample/Declarative/Axiom.lean diff --git a/Examples/Declarative/Class.lean b/LeanByExample/Declarative/Class.lean similarity index 100% rename from Examples/Declarative/Class.lean rename to LeanByExample/Declarative/Class.lean diff --git a/Examples/Declarative/DeclareSyntaxCat.lean b/LeanByExample/Declarative/DeclareSyntaxCat.lean similarity index 100% rename from Examples/Declarative/DeclareSyntaxCat.lean rename to LeanByExample/Declarative/DeclareSyntaxCat.lean diff --git a/Examples/Declarative/Def.lean b/LeanByExample/Declarative/Def.lean similarity index 100% rename from Examples/Declarative/Def.lean rename to LeanByExample/Declarative/Def.lean diff --git a/Examples/Declarative/Deriving.lean b/LeanByExample/Declarative/Deriving.lean similarity index 100% rename from Examples/Declarative/Deriving.lean rename to LeanByExample/Declarative/Deriving.lean diff --git a/Examples/Declarative/Elab.lean b/LeanByExample/Declarative/Elab.lean similarity index 100% rename from Examples/Declarative/Elab.lean rename to LeanByExample/Declarative/Elab.lean diff --git a/Examples/Declarative/Example.lean b/LeanByExample/Declarative/Example.lean similarity index 100% rename from Examples/Declarative/Example.lean rename to LeanByExample/Declarative/Example.lean diff --git a/Examples/Declarative/Export.lean b/LeanByExample/Declarative/Export.lean similarity index 100% rename from Examples/Declarative/Export.lean rename to LeanByExample/Declarative/Export.lean diff --git a/Examples/Declarative/Inductive.lean b/LeanByExample/Declarative/Inductive.lean similarity index 100% rename from Examples/Declarative/Inductive.lean rename to LeanByExample/Declarative/Inductive.lean diff --git a/Examples/Declarative/Infix.lean b/LeanByExample/Declarative/Infix.lean similarity index 100% rename from Examples/Declarative/Infix.lean rename to LeanByExample/Declarative/Infix.lean diff --git a/Examples/Declarative/Instance.lean b/LeanByExample/Declarative/Instance.lean similarity index 100% rename from Examples/Declarative/Instance.lean rename to LeanByExample/Declarative/Instance.lean diff --git a/Examples/Declarative/Local.lean b/LeanByExample/Declarative/Local.lean similarity index 100% rename from Examples/Declarative/Local.lean rename to LeanByExample/Declarative/Local.lean diff --git a/Examples/Declarative/Macro.lean b/LeanByExample/Declarative/Macro.lean similarity index 100% rename from Examples/Declarative/Macro.lean rename to LeanByExample/Declarative/Macro.lean diff --git a/Examples/Declarative/MacroRules.lean b/LeanByExample/Declarative/MacroRules.lean similarity index 100% rename from Examples/Declarative/MacroRules.lean rename to LeanByExample/Declarative/MacroRules.lean diff --git a/Examples/Declarative/Namespace.lean b/LeanByExample/Declarative/Namespace.lean similarity index 100% rename from Examples/Declarative/Namespace.lean rename to LeanByExample/Declarative/Namespace.lean diff --git a/Examples/Declarative/Noncomputable.lean b/LeanByExample/Declarative/Noncomputable.lean similarity index 100% rename from Examples/Declarative/Noncomputable.lean rename to LeanByExample/Declarative/Noncomputable.lean diff --git a/Examples/Declarative/Notation.lean b/LeanByExample/Declarative/Notation.lean similarity index 100% rename from Examples/Declarative/Notation.lean rename to LeanByExample/Declarative/Notation.lean diff --git a/Examples/Declarative/Opaque.lean b/LeanByExample/Declarative/Opaque.lean similarity index 100% rename from Examples/Declarative/Opaque.lean rename to LeanByExample/Declarative/Opaque.lean diff --git a/Examples/Declarative/Open.lean b/LeanByExample/Declarative/Open.lean similarity index 100% rename from Examples/Declarative/Open.lean rename to LeanByExample/Declarative/Open.lean diff --git a/Examples/Declarative/Partial.lean b/LeanByExample/Declarative/Partial.lean similarity index 100% rename from Examples/Declarative/Partial.lean rename to LeanByExample/Declarative/Partial.lean diff --git a/Examples/Declarative/Postfix.lean b/LeanByExample/Declarative/Postfix.lean similarity index 100% rename from Examples/Declarative/Postfix.lean rename to LeanByExample/Declarative/Postfix.lean diff --git a/Examples/Declarative/Prefix.lean b/LeanByExample/Declarative/Prefix.lean similarity index 100% rename from Examples/Declarative/Prefix.lean rename to LeanByExample/Declarative/Prefix.lean diff --git a/Examples/Declarative/Private.lean b/LeanByExample/Declarative/Private.lean similarity index 100% rename from Examples/Declarative/Private.lean rename to LeanByExample/Declarative/Private.lean diff --git a/Examples/Declarative/ProofWanted.lean b/LeanByExample/Declarative/ProofWanted.lean similarity index 100% rename from Examples/Declarative/ProofWanted.lean rename to LeanByExample/Declarative/ProofWanted.lean diff --git a/Examples/Declarative/Protected.lean b/LeanByExample/Declarative/Protected.lean similarity index 100% rename from Examples/Declarative/Protected.lean rename to LeanByExample/Declarative/Protected.lean diff --git a/Examples/Declarative/README.lean b/LeanByExample/Declarative/README.lean similarity index 100% rename from Examples/Declarative/README.lean rename to LeanByExample/Declarative/README.lean diff --git a/Examples/Declarative/Scoped.lean b/LeanByExample/Declarative/Scoped.lean similarity index 100% rename from Examples/Declarative/Scoped.lean rename to LeanByExample/Declarative/Scoped.lean diff --git a/Examples/Declarative/Section.lean b/LeanByExample/Declarative/Section.lean similarity index 100% rename from Examples/Declarative/Section.lean rename to LeanByExample/Declarative/Section.lean diff --git a/Examples/Declarative/SetOption.lean b/LeanByExample/Declarative/SetOption.lean similarity index 100% rename from Examples/Declarative/SetOption.lean rename to LeanByExample/Declarative/SetOption.lean diff --git a/Examples/Declarative/Structure.lean b/LeanByExample/Declarative/Structure.lean similarity index 100% rename from Examples/Declarative/Structure.lean rename to LeanByExample/Declarative/Structure.lean diff --git a/Examples/Declarative/Syntax.lean b/LeanByExample/Declarative/Syntax.lean similarity index 100% rename from Examples/Declarative/Syntax.lean rename to LeanByExample/Declarative/Syntax.lean diff --git a/Examples/Declarative/TerminationBy.lean b/LeanByExample/Declarative/TerminationBy.lean similarity index 100% rename from Examples/Declarative/TerminationBy.lean rename to LeanByExample/Declarative/TerminationBy.lean diff --git a/Examples/Declarative/Theorem.lean b/LeanByExample/Declarative/Theorem.lean similarity index 100% rename from Examples/Declarative/Theorem.lean rename to LeanByExample/Declarative/Theorem.lean diff --git a/Examples/Declarative/Variable.lean b/LeanByExample/Declarative/Variable.lean similarity index 100% rename from Examples/Declarative/Variable.lean rename to LeanByExample/Declarative/Variable.lean diff --git a/Examples/Diagnostic/Check.lean b/LeanByExample/Diagnostic/Check.lean similarity index 100% rename from Examples/Diagnostic/Check.lean rename to LeanByExample/Diagnostic/Check.lean diff --git a/Examples/Diagnostic/CheckFailure.lean b/LeanByExample/Diagnostic/CheckFailure.lean similarity index 100% rename from Examples/Diagnostic/CheckFailure.lean rename to LeanByExample/Diagnostic/CheckFailure.lean diff --git a/Examples/Diagnostic/Eval.lean b/LeanByExample/Diagnostic/Eval.lean similarity index 100% rename from Examples/Diagnostic/Eval.lean rename to LeanByExample/Diagnostic/Eval.lean diff --git a/Examples/Diagnostic/Find.lean b/LeanByExample/Diagnostic/Find.lean similarity index 100% rename from Examples/Diagnostic/Find.lean rename to LeanByExample/Diagnostic/Find.lean diff --git a/Examples/Diagnostic/Guard.lean b/LeanByExample/Diagnostic/Guard.lean similarity index 100% rename from Examples/Diagnostic/Guard.lean rename to LeanByExample/Diagnostic/Guard.lean diff --git a/Examples/Diagnostic/GuardMsgs.lean b/LeanByExample/Diagnostic/GuardMsgs.lean similarity index 100% rename from Examples/Diagnostic/GuardMsgs.lean rename to LeanByExample/Diagnostic/GuardMsgs.lean diff --git a/Examples/Diagnostic/Help.lean b/LeanByExample/Diagnostic/Help.lean similarity index 100% rename from Examples/Diagnostic/Help.lean rename to LeanByExample/Diagnostic/Help.lean diff --git a/Examples/Diagnostic/Instances.lean b/LeanByExample/Diagnostic/Instances.lean similarity index 100% rename from Examples/Diagnostic/Instances.lean rename to LeanByExample/Diagnostic/Instances.lean diff --git a/Examples/Diagnostic/Print.lean b/LeanByExample/Diagnostic/Print.lean similarity index 100% rename from Examples/Diagnostic/Print.lean rename to LeanByExample/Diagnostic/Print.lean diff --git a/Examples/Diagnostic/README.lean b/LeanByExample/Diagnostic/README.lean similarity index 100% rename from Examples/Diagnostic/README.lean rename to LeanByExample/Diagnostic/README.lean diff --git a/Examples/Diagnostic/Reduce.lean b/LeanByExample/Diagnostic/Reduce.lean similarity index 100% rename from Examples/Diagnostic/Reduce.lean rename to LeanByExample/Diagnostic/Reduce.lean diff --git a/Examples/Diagnostic/Synth.lean b/LeanByExample/Diagnostic/Synth.lean similarity index 100% rename from Examples/Diagnostic/Synth.lean rename to LeanByExample/Diagnostic/Synth.lean diff --git a/Examples/Diagnostic/Time.lean b/LeanByExample/Diagnostic/Time.lean similarity index 100% rename from Examples/Diagnostic/Time.lean rename to LeanByExample/Diagnostic/Time.lean diff --git a/Examples/Diagnostic/Whnf.lean b/LeanByExample/Diagnostic/Whnf.lean similarity index 100% rename from Examples/Diagnostic/Whnf.lean rename to LeanByExample/Diagnostic/Whnf.lean diff --git a/Examples/Option/AutoImplicit.lean b/LeanByExample/Option/AutoImplicit.lean similarity index 100% rename from Examples/Option/AutoImplicit.lean rename to LeanByExample/Option/AutoImplicit.lean diff --git a/Examples/Option/Flexible.lean b/LeanByExample/Option/Flexible.lean similarity index 100% rename from Examples/Option/Flexible.lean rename to LeanByExample/Option/Flexible.lean diff --git a/Examples/Option/Hygiene.lean b/LeanByExample/Option/Hygiene.lean similarity index 100% rename from Examples/Option/Hygiene.lean rename to LeanByExample/Option/Hygiene.lean diff --git a/Examples/Option/README.lean b/LeanByExample/Option/README.lean similarity index 100% rename from Examples/Option/README.lean rename to LeanByExample/Option/README.lean diff --git a/Examples/Solution/BarberParadox.lean b/LeanByExample/Solution/BarberParadox.lean similarity index 100% rename from Examples/Solution/BarberParadox.lean rename to LeanByExample/Solution/BarberParadox.lean diff --git a/Examples/Solution/CantorPairing.lean b/LeanByExample/Solution/CantorPairing.lean similarity index 100% rename from Examples/Solution/CantorPairing.lean rename to LeanByExample/Solution/CantorPairing.lean diff --git a/Examples/Solution/CantorTheorem.lean b/LeanByExample/Solution/CantorTheorem.lean similarity index 100% rename from Examples/Solution/CantorTheorem.lean rename to LeanByExample/Solution/CantorTheorem.lean diff --git a/Examples/Solution/DoubtImplication.lean b/LeanByExample/Solution/DoubtImplication.lean similarity index 100% rename from Examples/Solution/DoubtImplication.lean rename to LeanByExample/Solution/DoubtImplication.lean diff --git a/Examples/Solution/HeytingAndBooleanAlgebra.lean b/LeanByExample/Solution/HeytingAndBooleanAlgebra.lean similarity index 100% rename from Examples/Solution/HeytingAndBooleanAlgebra.lean rename to LeanByExample/Solution/HeytingAndBooleanAlgebra.lean diff --git a/Examples/Solution/InverseSurjInj.lean b/LeanByExample/Solution/InverseSurjInj.lean similarity index 100% rename from Examples/Solution/InverseSurjInj.lean rename to LeanByExample/Solution/InverseSurjInj.lean diff --git a/Examples/Solution/KnightAndKnave.lean b/LeanByExample/Solution/KnightAndKnave.lean similarity index 100% rename from Examples/Solution/KnightAndKnave.lean rename to LeanByExample/Solution/KnightAndKnave.lean diff --git a/Examples/Solution/README.lean b/LeanByExample/Solution/README.lean similarity index 100% rename from Examples/Solution/README.lean rename to LeanByExample/Solution/README.lean diff --git a/Examples/Tactic/AcRfl.lean b/LeanByExample/Tactic/AcRfl.lean similarity index 100% rename from Examples/Tactic/AcRfl.lean rename to LeanByExample/Tactic/AcRfl.lean diff --git a/Examples/Tactic/Aesop.lean b/LeanByExample/Tactic/Aesop.lean similarity index 100% rename from Examples/Tactic/Aesop.lean rename to LeanByExample/Tactic/Aesop.lean diff --git a/Examples/Tactic/AllGoals.lean b/LeanByExample/Tactic/AllGoals.lean similarity index 100% rename from Examples/Tactic/AllGoals.lean rename to LeanByExample/Tactic/AllGoals.lean diff --git a/Examples/Tactic/Apply.lean b/LeanByExample/Tactic/Apply.lean similarity index 100% rename from Examples/Tactic/Apply.lean rename to LeanByExample/Tactic/Apply.lean diff --git a/Examples/Tactic/ApplyAssumption.lean b/LeanByExample/Tactic/ApplyAssumption.lean similarity index 100% rename from Examples/Tactic/ApplyAssumption.lean rename to LeanByExample/Tactic/ApplyAssumption.lean diff --git a/Examples/Tactic/ApplyAt.lean b/LeanByExample/Tactic/ApplyAt.lean similarity index 100% rename from Examples/Tactic/ApplyAt.lean rename to LeanByExample/Tactic/ApplyAt.lean diff --git a/Examples/Tactic/ApplyQuestion.lean b/LeanByExample/Tactic/ApplyQuestion.lean similarity index 100% rename from Examples/Tactic/ApplyQuestion.lean rename to LeanByExample/Tactic/ApplyQuestion.lean diff --git a/Examples/Tactic/Assumption.lean b/LeanByExample/Tactic/Assumption.lean similarity index 100% rename from Examples/Tactic/Assumption.lean rename to LeanByExample/Tactic/Assumption.lean diff --git a/Examples/Tactic/By.lean b/LeanByExample/Tactic/By.lean similarity index 100% rename from Examples/Tactic/By.lean rename to LeanByExample/Tactic/By.lean diff --git a/Examples/Tactic/ByCases.lean b/LeanByExample/Tactic/ByCases.lean similarity index 100% rename from Examples/Tactic/ByCases.lean rename to LeanByExample/Tactic/ByCases.lean diff --git a/Examples/Tactic/ByContra.lean b/LeanByExample/Tactic/ByContra.lean similarity index 100% rename from Examples/Tactic/ByContra.lean rename to LeanByExample/Tactic/ByContra.lean diff --git a/Examples/Tactic/Calc.lean b/LeanByExample/Tactic/Calc.lean similarity index 100% rename from Examples/Tactic/Calc.lean rename to LeanByExample/Tactic/Calc.lean diff --git a/Examples/Tactic/Cases.lean b/LeanByExample/Tactic/Cases.lean similarity index 100% rename from Examples/Tactic/Cases.lean rename to LeanByExample/Tactic/Cases.lean diff --git a/Examples/Tactic/CasesAp.lean b/LeanByExample/Tactic/CasesAp.lean similarity index 100% rename from Examples/Tactic/CasesAp.lean rename to LeanByExample/Tactic/CasesAp.lean diff --git a/Examples/Tactic/Choose.lean b/LeanByExample/Tactic/Choose.lean similarity index 100% rename from Examples/Tactic/Choose.lean rename to LeanByExample/Tactic/Choose.lean diff --git a/Examples/Tactic/Clear.lean b/LeanByExample/Tactic/Clear.lean similarity index 100% rename from Examples/Tactic/Clear.lean rename to LeanByExample/Tactic/Clear.lean diff --git a/Examples/Tactic/Congr.lean b/LeanByExample/Tactic/Congr.lean similarity index 100% rename from Examples/Tactic/Congr.lean rename to LeanByExample/Tactic/Congr.lean diff --git a/Examples/Tactic/Constructor.lean b/LeanByExample/Tactic/Constructor.lean similarity index 100% rename from Examples/Tactic/Constructor.lean rename to LeanByExample/Tactic/Constructor.lean diff --git a/Examples/Tactic/Contradiction.lean b/LeanByExample/Tactic/Contradiction.lean similarity index 100% rename from Examples/Tactic/Contradiction.lean rename to LeanByExample/Tactic/Contradiction.lean diff --git a/Examples/Tactic/Contrapose.lean b/LeanByExample/Tactic/Contrapose.lean similarity index 100% rename from Examples/Tactic/Contrapose.lean rename to LeanByExample/Tactic/Contrapose.lean diff --git a/Examples/Tactic/Conv.lean b/LeanByExample/Tactic/Conv.lean similarity index 100% rename from Examples/Tactic/Conv.lean rename to LeanByExample/Tactic/Conv.lean diff --git a/Examples/Tactic/Convert.lean b/LeanByExample/Tactic/Convert.lean similarity index 100% rename from Examples/Tactic/Convert.lean rename to LeanByExample/Tactic/Convert.lean diff --git a/Examples/Tactic/Decide.lean b/LeanByExample/Tactic/Decide.lean similarity index 100% rename from Examples/Tactic/Decide.lean rename to LeanByExample/Tactic/Decide.lean diff --git a/Examples/Tactic/Done.lean b/LeanByExample/Tactic/Done.lean similarity index 100% rename from Examples/Tactic/Done.lean rename to LeanByExample/Tactic/Done.lean diff --git a/Examples/Tactic/Dsimp.lean b/LeanByExample/Tactic/Dsimp.lean similarity index 100% rename from Examples/Tactic/Dsimp.lean rename to LeanByExample/Tactic/Dsimp.lean diff --git a/Examples/Tactic/Exact.lean b/LeanByExample/Tactic/Exact.lean similarity index 100% rename from Examples/Tactic/Exact.lean rename to LeanByExample/Tactic/Exact.lean diff --git a/Examples/Tactic/ExactQuestion.lean b/LeanByExample/Tactic/ExactQuestion.lean similarity index 100% rename from Examples/Tactic/ExactQuestion.lean rename to LeanByExample/Tactic/ExactQuestion.lean diff --git a/Examples/Tactic/Exfalso.lean b/LeanByExample/Tactic/Exfalso.lean similarity index 100% rename from Examples/Tactic/Exfalso.lean rename to LeanByExample/Tactic/Exfalso.lean diff --git a/Examples/Tactic/Exists.lean b/LeanByExample/Tactic/Exists.lean similarity index 100% rename from Examples/Tactic/Exists.lean rename to LeanByExample/Tactic/Exists.lean diff --git a/Examples/Tactic/Ext.lean b/LeanByExample/Tactic/Ext.lean similarity index 100% rename from Examples/Tactic/Ext.lean rename to LeanByExample/Tactic/Ext.lean diff --git a/Examples/Tactic/FieldSimp.lean b/LeanByExample/Tactic/FieldSimp.lean similarity index 100% rename from Examples/Tactic/FieldSimp.lean rename to LeanByExample/Tactic/FieldSimp.lean diff --git a/Examples/Tactic/FinCases.lean b/LeanByExample/Tactic/FinCases.lean similarity index 100% rename from Examples/Tactic/FinCases.lean rename to LeanByExample/Tactic/FinCases.lean diff --git a/Examples/Tactic/FunProp.lean b/LeanByExample/Tactic/FunProp.lean similarity index 100% rename from Examples/Tactic/FunProp.lean rename to LeanByExample/Tactic/FunProp.lean diff --git a/Examples/Tactic/Funext.lean b/LeanByExample/Tactic/Funext.lean similarity index 100% rename from Examples/Tactic/Funext.lean rename to LeanByExample/Tactic/Funext.lean diff --git a/Examples/Tactic/Gcongr.lean b/LeanByExample/Tactic/Gcongr.lean similarity index 100% rename from Examples/Tactic/Gcongr.lean rename to LeanByExample/Tactic/Gcongr.lean diff --git a/Examples/Tactic/Generalize.lean b/LeanByExample/Tactic/Generalize.lean similarity index 100% rename from Examples/Tactic/Generalize.lean rename to LeanByExample/Tactic/Generalize.lean diff --git a/Examples/Tactic/GuardHyp.lean b/LeanByExample/Tactic/GuardHyp.lean similarity index 100% rename from Examples/Tactic/GuardHyp.lean rename to LeanByExample/Tactic/GuardHyp.lean diff --git a/Examples/Tactic/Have.lean b/LeanByExample/Tactic/Have.lean similarity index 100% rename from Examples/Tactic/Have.lean rename to LeanByExample/Tactic/Have.lean diff --git a/Examples/Tactic/Hint.lean b/LeanByExample/Tactic/Hint.lean similarity index 100% rename from Examples/Tactic/Hint.lean rename to LeanByExample/Tactic/Hint.lean diff --git a/Examples/Tactic/Induction.lean b/LeanByExample/Tactic/Induction.lean similarity index 100% rename from Examples/Tactic/Induction.lean rename to LeanByExample/Tactic/Induction.lean diff --git a/Examples/Tactic/InductionAp.lean b/LeanByExample/Tactic/InductionAp.lean similarity index 100% rename from Examples/Tactic/InductionAp.lean rename to LeanByExample/Tactic/InductionAp.lean diff --git a/Examples/Tactic/Intro.lean b/LeanByExample/Tactic/Intro.lean similarity index 100% rename from Examples/Tactic/Intro.lean rename to LeanByExample/Tactic/Intro.lean diff --git a/Examples/Tactic/Itauto.lean b/LeanByExample/Tactic/Itauto.lean similarity index 100% rename from Examples/Tactic/Itauto.lean rename to LeanByExample/Tactic/Itauto.lean diff --git a/Examples/Tactic/Left.lean b/LeanByExample/Tactic/Left.lean similarity index 100% rename from Examples/Tactic/Left.lean rename to LeanByExample/Tactic/Left.lean diff --git a/Examples/Tactic/Linarith.lean b/LeanByExample/Tactic/Linarith.lean similarity index 100% rename from Examples/Tactic/Linarith.lean rename to LeanByExample/Tactic/Linarith.lean diff --git a/Examples/Tactic/NativeDecide.lean b/LeanByExample/Tactic/NativeDecide.lean similarity index 100% rename from Examples/Tactic/NativeDecide.lean rename to LeanByExample/Tactic/NativeDecide.lean diff --git a/Examples/Tactic/Nlinarith.lean b/LeanByExample/Tactic/Nlinarith.lean similarity index 100% rename from Examples/Tactic/Nlinarith.lean rename to LeanByExample/Tactic/Nlinarith.lean diff --git a/Examples/Tactic/NormCast.lean b/LeanByExample/Tactic/NormCast.lean similarity index 100% rename from Examples/Tactic/NormCast.lean rename to LeanByExample/Tactic/NormCast.lean diff --git a/Examples/Tactic/NthRw.lean b/LeanByExample/Tactic/NthRw.lean similarity index 100% rename from Examples/Tactic/NthRw.lean rename to LeanByExample/Tactic/NthRw.lean diff --git a/Examples/Tactic/Obtain.lean b/LeanByExample/Tactic/Obtain.lean similarity index 100% rename from Examples/Tactic/Obtain.lean rename to LeanByExample/Tactic/Obtain.lean diff --git a/Examples/Tactic/Omega.lean b/LeanByExample/Tactic/Omega.lean similarity index 100% rename from Examples/Tactic/Omega.lean rename to LeanByExample/Tactic/Omega.lean diff --git a/Examples/Tactic/Positivity.lean b/LeanByExample/Tactic/Positivity.lean similarity index 100% rename from Examples/Tactic/Positivity.lean rename to LeanByExample/Tactic/Positivity.lean diff --git a/Examples/Tactic/PushNeg.lean b/LeanByExample/Tactic/PushNeg.lean similarity index 100% rename from Examples/Tactic/PushNeg.lean rename to LeanByExample/Tactic/PushNeg.lean diff --git a/Examples/Tactic/Qify.lean b/LeanByExample/Tactic/Qify.lean similarity index 100% rename from Examples/Tactic/Qify.lean rename to LeanByExample/Tactic/Qify.lean diff --git a/Examples/Tactic/README.lean b/LeanByExample/Tactic/README.lean similarity index 100% rename from Examples/Tactic/README.lean rename to LeanByExample/Tactic/README.lean diff --git a/Examples/Tactic/Rcases.lean b/LeanByExample/Tactic/Rcases.lean similarity index 100% rename from Examples/Tactic/Rcases.lean rename to LeanByExample/Tactic/Rcases.lean diff --git a/Examples/Tactic/Refine.lean b/LeanByExample/Tactic/Refine.lean similarity index 100% rename from Examples/Tactic/Refine.lean rename to LeanByExample/Tactic/Refine.lean diff --git a/Examples/Tactic/Rel.lean b/LeanByExample/Tactic/Rel.lean similarity index 100% rename from Examples/Tactic/Rel.lean rename to LeanByExample/Tactic/Rel.lean diff --git a/Examples/Tactic/RenameI.lean b/LeanByExample/Tactic/RenameI.lean similarity index 100% rename from Examples/Tactic/RenameI.lean rename to LeanByExample/Tactic/RenameI.lean diff --git a/Examples/Tactic/Repeat.lean b/LeanByExample/Tactic/Repeat.lean similarity index 100% rename from Examples/Tactic/Repeat.lean rename to LeanByExample/Tactic/Repeat.lean diff --git a/Examples/Tactic/Replace.lean b/LeanByExample/Tactic/Replace.lean similarity index 100% rename from Examples/Tactic/Replace.lean rename to LeanByExample/Tactic/Replace.lean diff --git a/Examples/Tactic/Rfl.lean b/LeanByExample/Tactic/Rfl.lean similarity index 100% rename from Examples/Tactic/Rfl.lean rename to LeanByExample/Tactic/Rfl.lean diff --git a/Examples/Tactic/Right.lean b/LeanByExample/Tactic/Right.lean similarity index 100% rename from Examples/Tactic/Right.lean rename to LeanByExample/Tactic/Right.lean diff --git a/Examples/Tactic/Ring.lean b/LeanByExample/Tactic/Ring.lean similarity index 100% rename from Examples/Tactic/Ring.lean rename to LeanByExample/Tactic/Ring.lean diff --git a/Examples/Tactic/Rw.lean b/LeanByExample/Tactic/Rw.lean similarity index 100% rename from Examples/Tactic/Rw.lean rename to LeanByExample/Tactic/Rw.lean diff --git a/Examples/Tactic/RwSearch.lean b/LeanByExample/Tactic/RwSearch.lean similarity index 100% rename from Examples/Tactic/RwSearch.lean rename to LeanByExample/Tactic/RwSearch.lean diff --git a/Examples/Tactic/Says.lean b/LeanByExample/Tactic/Says.lean similarity index 100% rename from Examples/Tactic/Says.lean rename to LeanByExample/Tactic/Says.lean diff --git a/Examples/Tactic/SeqFocus.lean b/LeanByExample/Tactic/SeqFocus.lean similarity index 100% rename from Examples/Tactic/SeqFocus.lean rename to LeanByExample/Tactic/SeqFocus.lean diff --git a/Examples/Tactic/Set.lean b/LeanByExample/Tactic/Set.lean similarity index 100% rename from Examples/Tactic/Set.lean rename to LeanByExample/Tactic/Set.lean diff --git a/Examples/Tactic/Show.lean b/LeanByExample/Tactic/Show.lean similarity index 100% rename from Examples/Tactic/Show.lean rename to LeanByExample/Tactic/Show.lean diff --git a/Examples/Tactic/Simp.lean b/LeanByExample/Tactic/Simp.lean similarity index 100% rename from Examples/Tactic/Simp.lean rename to LeanByExample/Tactic/Simp.lean diff --git a/Examples/Tactic/SlimCheck.lean b/LeanByExample/Tactic/SlimCheck.lean similarity index 100% rename from Examples/Tactic/SlimCheck.lean rename to LeanByExample/Tactic/SlimCheck.lean diff --git a/Examples/Tactic/Sorry.lean b/LeanByExample/Tactic/Sorry.lean similarity index 100% rename from Examples/Tactic/Sorry.lean rename to LeanByExample/Tactic/Sorry.lean diff --git a/Examples/Tactic/Split.lean b/LeanByExample/Tactic/Split.lean similarity index 100% rename from Examples/Tactic/Split.lean rename to LeanByExample/Tactic/Split.lean diff --git a/Examples/Tactic/Suffices.lean b/LeanByExample/Tactic/Suffices.lean similarity index 100% rename from Examples/Tactic/Suffices.lean rename to LeanByExample/Tactic/Suffices.lean diff --git a/Examples/Tactic/Tauto.lean b/LeanByExample/Tactic/Tauto.lean similarity index 100% rename from Examples/Tactic/Tauto.lean rename to LeanByExample/Tactic/Tauto.lean diff --git a/Examples/Tactic/Trans.lean b/LeanByExample/Tactic/Trans.lean similarity index 100% rename from Examples/Tactic/Trans.lean rename to LeanByExample/Tactic/Trans.lean diff --git a/Examples/Tactic/Trivial.lean b/LeanByExample/Tactic/Trivial.lean similarity index 100% rename from Examples/Tactic/Trivial.lean rename to LeanByExample/Tactic/Trivial.lean diff --git a/Examples/Tactic/Try.lean b/LeanByExample/Tactic/Try.lean similarity index 100% rename from Examples/Tactic/Try.lean rename to LeanByExample/Tactic/Try.lean diff --git a/Examples/Tactic/Unfold.lean b/LeanByExample/Tactic/Unfold.lean similarity index 100% rename from Examples/Tactic/Unfold.lean rename to LeanByExample/Tactic/Unfold.lean diff --git a/Examples/Tactic/WithReducible.lean b/LeanByExample/Tactic/WithReducible.lean similarity index 100% rename from Examples/Tactic/WithReducible.lean rename to LeanByExample/Tactic/WithReducible.lean diff --git a/Examples/Tactic/Wlog.lean b/LeanByExample/Tactic/Wlog.lean similarity index 100% rename from Examples/Tactic/Wlog.lean rename to LeanByExample/Tactic/Wlog.lean diff --git a/Examples/Type/Char.lean b/LeanByExample/Type/Char.lean similarity index 100% rename from Examples/Type/Char.lean rename to LeanByExample/Type/Char.lean diff --git a/Examples/Type/Float.lean b/LeanByExample/Type/Float.lean similarity index 100% rename from Examples/Type/Float.lean rename to LeanByExample/Type/Float.lean diff --git a/Examples/Type/List.lean b/LeanByExample/Type/List.lean similarity index 100% rename from Examples/Type/List.lean rename to LeanByExample/Type/List.lean diff --git a/Examples/Type/Prop.lean b/LeanByExample/Type/Prop.lean similarity index 100% rename from Examples/Type/Prop.lean rename to LeanByExample/Type/Prop.lean diff --git a/Examples/Type/README.lean b/LeanByExample/Type/README.lean similarity index 100% rename from Examples/Type/README.lean rename to LeanByExample/Type/README.lean diff --git a/Examples/Type/String.lean b/LeanByExample/Type/String.lean similarity index 100% rename from Examples/Type/String.lean rename to LeanByExample/Type/String.lean diff --git a/Examples/Type/Type.lean b/LeanByExample/Type/Type.lean similarity index 100% rename from Examples/Type/Type.lean rename to LeanByExample/Type/Type.lean diff --git a/Examples/TypeClass/Coe.lean b/LeanByExample/TypeClass/Coe.lean similarity index 100% rename from Examples/TypeClass/Coe.lean rename to LeanByExample/TypeClass/Coe.lean diff --git a/Examples/TypeClass/CoeDep.lean b/LeanByExample/TypeClass/CoeDep.lean similarity index 100% rename from Examples/TypeClass/CoeDep.lean rename to LeanByExample/TypeClass/CoeDep.lean diff --git a/Examples/TypeClass/CoeFun.lean b/LeanByExample/TypeClass/CoeFun.lean similarity index 100% rename from Examples/TypeClass/CoeFun.lean rename to LeanByExample/TypeClass/CoeFun.lean diff --git a/Examples/TypeClass/CoeSort.lean b/LeanByExample/TypeClass/CoeSort.lean similarity index 100% rename from Examples/TypeClass/CoeSort.lean rename to LeanByExample/TypeClass/CoeSort.lean diff --git a/Examples/TypeClass/Decidable.lean b/LeanByExample/TypeClass/Decidable.lean similarity index 100% rename from Examples/TypeClass/Decidable.lean rename to LeanByExample/TypeClass/Decidable.lean diff --git a/Examples/TypeClass/GetElem.lean b/LeanByExample/TypeClass/GetElem.lean similarity index 100% rename from Examples/TypeClass/GetElem.lean rename to LeanByExample/TypeClass/GetElem.lean diff --git a/Examples/TypeClass/Inhabited.lean b/LeanByExample/TypeClass/Inhabited.lean similarity index 100% rename from Examples/TypeClass/Inhabited.lean rename to LeanByExample/TypeClass/Inhabited.lean diff --git a/Examples/TypeClass/OfNat.lean b/LeanByExample/TypeClass/OfNat.lean similarity index 100% rename from Examples/TypeClass/OfNat.lean rename to LeanByExample/TypeClass/OfNat.lean diff --git a/Examples/TypeClass/README.lean b/LeanByExample/TypeClass/README.lean similarity index 100% rename from Examples/TypeClass/README.lean rename to LeanByExample/TypeClass/README.lean diff --git a/Examples/TypeClass/Repr.lean b/LeanByExample/TypeClass/Repr.lean similarity index 100% rename from Examples/TypeClass/Repr.lean rename to LeanByExample/TypeClass/Repr.lean diff --git a/Examples/TypeClass/ToString.lean b/LeanByExample/TypeClass/ToString.lean similarity index 100% rename from Examples/TypeClass/ToString.lean rename to LeanByExample/TypeClass/ToString.lean diff --git a/assets/filePlay.js b/assets/filePlay.js index 00fcb816..9ea657da 100644 --- 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 index a841f3af..5174092f 100644 --- 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 index a3519bd6..ce47618a 100644 --- 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