Kitamado
Kitamado
The current directory should not be specified as the src directory. This causes a problem where the `.git` directory is copied into the `book` directory.
see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/the.20metaprogramming.20book/near/386542851 There seems to be an intentional error in the code, which will be an obstacle when you try to update Lean version later. As a way to indicate...
Add the button 'Run in Lean4 Playground' to all code blocks and each page. Clicking it will take you to the Lean 4 web. I don't know how useful this...
at [Expressions](https://leanprover-community.github.io/lean4-metaprogramming-book/md/main/03_expressions.html#expressions) > letE n t v b is a let binder (let ($n : $t) := $v in $b). I don't think there is a syntax for `let` followed...
### Problem  ### Steps 1. install mdbook 2. create SUMMARY.md 3. run `mdbook serve --open` ### Possible Solution(s) The button to go back to the previous chapter should not...
may I open a PR? see: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20tactics.20list.3F/near/433066915
### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues)....
### Description in Lean v4.7.0 and mathlib 4.7.0, this code success: (see https://github.com/Seasawher/v470playground/blob/main/V470playground/Basic.lean) ```lean import Mathlib.Tactic variable (n m : Nat) example (h : n + m = 0) :...
Please complete the following information about the language: - Name: lean4 - Website: https://leanprover.github.io/ - Language Version: 4 - Any comments: official release of Lean 4 has come! --- :+1:...
It would be nice if there was a function to support translation into other languages. The mdbook currently used for documentation does not support this.