feat: grind chapter

.github/workflows/ci.yml

@@ -56,7 +56,7 @@ jobs:
       - name: Install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 

.github/workflows/release-tag.yml

@@ -70,7 +70,7 @@ jobs:
       - name: Install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 

Manual.lean

@@ -16,6 +16,7 @@ import Manual.Axioms
 import Manual.Terms
 import Manual.Tactics
 import Manual.Simp
+import Manual.Grind
 import Manual.BasicTypes
 import Manual.BasicProps
 import Manual.NotationsMacros
@@ -92,6 +93,8 @@ Thus, this reference manual does not draw a barrier between the two aspects, but
 
 {include 0 Manual.Simp}
 
+{include 0 Manual.Grind}
+
 {include 0 Manual.BasicProps}
 
 {include 0 Manual.BasicTypes}