lean-ja · Seasawher · Jan 3, 2025 · Jan 3, 2025
@@ -51,7 +51,7 @@ jobs:
         uses: lycheeverse/lychee-action@v2
         with:
           fail: true
-          args: --base book .
+          args: booksrc --base booksrc
 
       - name: Upload artifact
         uses: actions/upload-pages-artifact@v3

@@ -1,8 +1,9 @@
-https://raw.githubusercontent.com/lean-ja/lean-by-example/.*
 https://adam.math.hhu.de/#/g/leanprover-community/NNG4
+https://dcbadge.limes.pink/api/server/*
+https://lean-forward.github.io/
 https://lean-lang.org/*
+https://leansearch.net/
 https://live.lean-lang.org/
+https://raw.githubusercontent.com/lean-ja/lean-by-example/.*
+https://recharts.org/en-US
 https://reservoir.lean-lang.org/
-https://dcbadge.limes.pink/api/server/*
-https://leansearch.net/
-https://lean-forward.github.io/
@@ -9,7 +9,7 @@
 * `#help command` で全コマンドのリストが見られます。
 * `#help term` ですべての term syntax の一覧が見られます。
 
-他にも機能がありますが、詳細は[Mathlib のドキュメント](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/HelpCmd.html)をご覧ください。
+他にも機能がありますが、詳細は[Batteriesのドキュメント](https://leanprover-community.github.io/mathlib4_docs/Batteries/Tactic/HelpCmd.html)をご覧ください。
 -/
 import Batteries.Tactic.HelpCmd
 

@@ -69,4 +69,4 @@ example (h : x = y) : x * y = (x ^ 2 + y ^ 2) / 2 := by
   rw [h]
   ring
 
-/- [^field]: 体とは、四則演算が定義されていて、ゼロでない要素で割り算ができるものを指します。-/
+/- [^field]: 体とは、四則演算が定義されていて、0 でない要素で割り算ができるものを指します。 -/
@@ -16,7 +16,7 @@ example (n : Nat) : n + 0 = n := by
     rfl
 
 /- ## by? 構文
-[`by`](./By.md) を `by?` に変えることでも、`show_term` を呼び出すことができます。-/
+[`by`](#{root}/Parser/By.md) を `by?` に変えることでも、`show_term` を呼び出すことができます。-/
 
 /-- info: Try this: Eq.refl (n + 0) -/
 #guard_msgs in
-Original file line number
+Diff line change
@@ Expand Up / @@ -69,4 +69,4 @@ example (h : x = y) : x * y = (x ^ 2 + y ^ 2) / 2 := by @@
       rw [h]
       ring
-    /- [^field]: 体とは、四則演算が定義されていて、ゼロでない要素で割り算ができるものを指します。-/
+    /- [^field]: 体とは、四則演算が定義されていて、0 でない要素で割り算ができるものを指します。 -/