lean4-metaprogramming-book icon indicating copy to clipboard operation
lean4-metaprogramming-book copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Avoid deprecated getMVarDecl etc.

Open JLimperg opened this issue 3 years ago • 0 comments
trafficstars

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.

JLimperg avatar Jul 26 '22 10:07 JLimperg