lean4-metaprogramming-book
lean4-metaprogramming-book copied to clipboard
Avoid deprecated getMVarDecl etc.
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.