leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
211 stars 50 forks source link

Avoid deprecated getMVarDecl etc. #68

Closed JLimperg closed 1 year ago

JLimperg commented 2 years ago

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.