Lean by Example に名前を変える(バージョン更新も行う)

.lycheeignore

@@ -1,2 +1,2 @@
-https://raw.githubusercontent.com/lean-ja/tactic-cheatsheet/.*
+https://raw.githubusercontent.com/lean-ja/lean-by-example/.*
 https://adam.math.hhu.de/#/g/leanprover-community/NNG4

README.md

@@ -1,10 +1,10 @@
 # README
 
-[![repo logo](./src/image/project_image.png)](https://github.com/wei/socialify)
+<!-- [![repo logo](./src/image/project_image.png)]() -->
 
-![workflow](https://github.com/lean-ja/tactic-cheatsheet/actions/workflows/ci.yml/badge.svg) ![workflow](https://github.com/lean-ja/tactic-cheatsheet/actions/workflows/deploy.yml/badge.svg) ![workflow](https://github.com/lean-ja/tactic-cheatsheet/actions/workflows/update.yml/badge.svg) [![](https://dcbadge.limes.pink/api/server/p32ZfnVawh?style=flat)](https://discord.gg/p32ZfnVawh)
+![workflow](https://github.com/lean-ja/lean-by-example/actions/workflows/ci.yml/badge.svg) ![workflow](https://github.com/lean-ja/lean-by-example/actions/workflows/deploy.yml/badge.svg) ![workflow](https://github.com/lean-ja/lean-by-example/actions/workflows/update.yml/badge.svg) [![](https://dcbadge.limes.pink/api/server/p32ZfnVawh?style=flat)](https://discord.gg/p32ZfnVawh)
 
-Lean4 の主要なタクティクを使いたい場面から逆引きできるようにまとめたリストです．Lean4 で数学理論の形式化をする際に使われる主要なライブラリである，mathlib のタクティクも紹介しています．
+プログラミング言語であるとともに定理証明支援系でもある Lean 言語と，その主要なライブラリの使い方を豊富なコード例とともに解説した資料です．
 
 ## CONTRIBUTING
 

book.toml

@@ -3,8 +3,8 @@ authors = ["Seasawher"]
 language = "ja"
 multilingual = false
 src = "src"
-title = "Lean4 タクティク逆引きリスト"
-description = "「普段の数学を Lean でどう実現するのか」という疑問にお答えするための，タクティク逆引きリストです."
+title = "Lean by Example"
+description = "プログラミング言語であるとともに定理証明支援系でもある Lean 言語と，その主要なライブラリの使い方を豊富なコード例とともに解説した資料です．"
 
 [build]
 create-missing = false
@@ -13,8 +13,8 @@ build-dir = "book"
 [output.html]
 additional-js = ["assets/blockPlay.js", "assets/filePlay.js", "assets/fzf.umd.js", "assets/elasticlunr.js"]
 no-section-label = true
-git-repository-url = "https://github.com/lean-ja/tactic-cheatsheet"
-edit-url-template = "https://raw.githubusercontent.com/lean-ja/tactic-cheatsheet/main/{path}"
+git-repository-url = "https://github.com/lean-ja/lean-by-example"
+edit-url-template = "https://raw.githubusercontent.com/lean-ja/lean-by-example/main/{path}"
 default-theme = "ayu"
 
 [output.html.fold]

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/Seasawher/mdgen",
    "type": "git",
    "subDir": null,
-   "rev": "c98c18fac8350be3d82f56dd1096dc2d4f314863",
+   "rev": "6a6a412465e82572f6e30385592eac52ab055c83",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "f96a34401de084c73c787ecb45b85d4fb47bb981",
+   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -31,7 +31,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05",
+   "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
+   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -67,7 +67,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "ceff16fcda840af2a6e00559c6feff20cf7af9a3",
+   "rev": "ae4167de90c3665843a3f997bb8361e109f99751",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc1
+leanprover/lean4:v4.9.0-rc2

src/README.md

@@ -1,8 +1,8 @@
-# Lean4 タクティク逆引きリスト
+# Lean by Example
 
-「普段の数学を Lean でどうやって実現するんだろう」という疑問に答えるために，Lean や Mathlib のよく使うタクティクをユースケースから逆引きできるようにまとめたリストです．より便利にするため，タクティクだけでなく基本的なコマンドも紹介しています．
+プログラミング言語であるとともに定理証明支援系でもある Lean 言語と，その主要なライブラリの使い方を豊富なコード例とともに解説した資料です．
 
-> この文書は lean-ja が管理しています．誤りのご指摘，ご提案などは [GitHub リポジトリ](https://github.com/lean-ja/tactic-cheatsheet)からお願いします．
+> この文書は lean-ja が管理しています．誤りのご指摘，ご提案などは [GitHub リポジトリ](https://github.com/lean-ja/lean-by-example)からお願いします．
 >
 > lean-ja の Discord サーバが[こちら](https://discord.gg/p32ZfnVawh)にあります．質問や相談などはこちらにどうぞ．
 

src/SUMMARY.md

@@ -1,6 +1,6 @@
 # Summary
 
-[Lean4 タクティク逆引きリスト](./README.md)
+[はじめに](./README.md)
 
 [リンク集](./links.md)