Closed lakesare closed 1 year ago
Oh, the API must have changed. What happens if you don't pass the `assertTypeCmd
argument?
It goes like this:
@lakesare I've bumped the toolchain and fixed that issue: https://github.com/arthurpaulino/lean4-metaprogramming-book/commit/ec355bba83e3d65db57952f13abc23a32cafd009
Make sure to check the indentation levels of your code because the try ...
needs to be deeper than liftTermElabM
That worked! Thanks for the note about the nesting level, that was also important.
I'm getting the following error in the Introduction#Building a command example.
My Lean version is "leanprover/lean4:nightly-2022-10-09". Does this look familiar?