lean4-metaprogramming-book
lean4-metaprogramming-book copied to clipboard
leanprover-community
I know I'm an idiot who can't use the internet, but search for me stubbornly refuses to give me the URL of the web-based version of this book. I'm always...
The mechanism used for delayed mvar assignments has changed in a recent nightly. We have a brief section on this in the MetaM chapter, so we should check whether the...
Note: I'm raising this issue mostly for bookkeeping purposes -- if someone wants to address them please feel free to! (Anyways, I'm probably going to come back and add these...
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...
Exporting the book in > >A PDF is [available here for download](../../releases/download/latest/Metaprogramming.in.Lean.4.pdf) (and is rebuilt on each change). > Is generating a PDF which does not contain the images. A...
I found two typos in the `MetaM` chapter of the online version of the book: 1. In the first example using `Eq.trans`, the sentence "Now the third apply comes in....
The implementation (and description) of `` is wrong: it should only apply the second tactic to goals produced by the first tactic (implementation is missing a `focus`).
