Closed Seasawher closed 3 months ago
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?
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.
@Julian Review please.
Looks good I think. Thanks again!
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.
#guard_msgs
. Use--#
to ensure that they don't remain in markdown.#check_failure
.This PR pointed out where errors can be avoided simply by using
#check_failure
.I would like to hear your views on wherecheck_failure
cannot be used.Thank you.