Kitamado comments

Results 16 comments of


                                            Kitamado

put link to html version of book in README

What is the current status of this matter? I hope that a web version will be made available.

mdbook serve doesn't work in Docker

I experienced the same problem. I'm wondering how I can solve this problem.

fix issue on mdbook config

@Julian I don't know why the build of the PDF fails. Could you help me, please?

fix issue on mdbook config

memo: expected out put of `$(grep ...)` command: ```txt md/main/01_intro.md md/main/02_overview.md ``` correct command: ```bash grep -o '$\/.*\.md$' md/SUMMARY.md | sed 's/^/md/' ```

fix issue on mdbook config

this PR also fix issue https://github.com/leanprover-community/lean4-metaprogramming-book/pull/121#discussion_r1447642044

use `#check_failure` command to erase errors

Thanks for your comment. * I haven't read this book thoroughly either, so maybe I should read it properly before submitting a PR again. * You are right, if we...

use `#check_failure` command to erase errors

@Julian Review please.

can't see goal state after case tactic

`suffices ... by` notation has same issue. (Lean version: v4.8.0-rc1) ```lean example {a b : Nat} (h : a = b) : b ≤ b + 1 := by suffices...

Create a standard GitHub action for Lean projects

I thought it would be nice to include caching the `.lake` directory in the CI. Would this not contribute to increased speeds?

Create a standard GitHub action for Lean projects

Why not include lean update actions in this as well? Actions that automatically update Lean and mathlib versions should be in demand, as Lean is frequently updated.