Introduction chapter: Getting an error on assertTypeCmd in Lean4

[lakesare]

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?

[arthurpaulino]

Oh, the API must have changed. What happens if you don't pass the `assertTypeCmd argument?

[lakesare]

It goes like this:

[arthurpaulino]

@lakesare I've bumped the toolchain and fixed that issue: ec355bb

Make sure to check the indentation levels of your code because the try ... needs to be deeper than liftTermElabM

[lakesare]

That worked! Thanks for the note about the nesting level, that was also important.