ディレクトリ名変更: Examples → LeanByExample

Author: Seasawher

.github/CONTRIBUTING.md

@@ -36,7 +36,7 @@
   "material-icon-theme.folders.associations": {
     "booksrc": "markdown",
     "Command": "",
-    "Examples": "Content",
+    "LeanByExample": "Content",
     "Option": "",
   },
 

.vscode/settings.json

@@ -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/",
   );
 

Examples/Attribute/AppUnexpander.lean renamed to LeanByExample/Attribute/AppUnexpander.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"

Examples/Attribute/CasesEliminator.lean renamed to LeanByExample/Attribute/CasesEliminator.lean

@@ -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