lean4-metaprogramming-book
lean4-metaprogramming-book copied to clipboard
leanprover-community
Just leaving this here as a note to myself (or to anyone else who wants to do this of course). I think this would be very helpful. I'm thinking of...
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Metaprogramming.20tutorial/near/285465861
but instead use `$_` on the match, @sullrich just added a [linter](https://github.com/leanprover/lean4/pull/1381) for this.
@arthurpaulino Suggestions on what we want to teach when it comes to attributes would be nice. I haven't used attributes much, so I'm learning as I go along!
Create a simpler version of the attribute tutorial by covering whatever Leo did at the post ICERM hackathon.
The MetaM chapter already contains some notes about matching expressions up to computation, using `whnf`. But arguably the more convenient approach is to use `isDefEq` with a pattern expression containing...
Another note to self: mention these functions somewhere in the MetaM chapter. There's not much to discuss, but this functionality is obviously important, so people should be able to discover...
Many basic functions have changed recently, e.g. `getMVarDecl` to `MVarId.getDecl`. The old versions are deprecated, so we (I) should update the book accordingly. See leanprover/lean4#1346.
`and_then` is subtly different from `<;>`. The former focuses the goal, whereas the latter does not.
Page 60 suggests that `a and_then b` behaves the same as `a b`, but this is not the case when `b` does not close all goals; For example, if the...
