use `#check_failure` command to erase errors

[Seasawher]

trafficstars

see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/the.20metaprogramming.20book/near/386542851

There seems to be an intentional error in the code, which will be an obstacle when you try to update Lean version later.

As a way to indicate errors while avoiding them, I suggest the following.

• Import std and use #guard_msgs. Use --# to ensure that they don't remain in markdown.
• Use #check_failure.
• comment out the relevant section.

This PR pointed out where errors can be avoided simply by using #check_failure.I would like to hear your views on where check_failure cannot be used.

Thank you.

[Julian]

As I mentioned in Zulip I'm not 100% comfortable here given I actually have not read the book yet :D -- if no one else chimes in I'm comfortable enough though that you know the right thing :) given your contributions -- but I do think if we use these that the text of the book should at least mention what #check_failure does in an aside, in case the reader isn't familiar with what it's for. Does that make sense?

[Seasawher]

Thanks for your comment.

• I haven't read this book thoroughly either, so maybe I should read it properly before submitting a PR again.

• You are right, if we use check_failure, we should mention it somewhere in the text.

[Seasawher]

@Julian Review please.

[Julian]

Looks good I think. Thanks again!