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

Published 20 hours ago • verified publisher icon leanprover-community

Typo in `MetaM` chapter: the signature of `Lean.commitIfNoEx` is wrong

Open spinylobster opened this issue 1 year ago • 0 comments
trafficstars

in https://leanprover-community.github.io/lean4-metaprogramming-book/main/04_metam.html#backtracking ,

Lean.commitIfNoEx (x : α) : m α executes x. If x succeeds, commitIfNoEx returns its result. If x throws an exception, commitIfNoEx backtracks the state and rethrows the exception.

the actual signature is Lean.commitIfNoEx (x : m α) : m α.

spinylobster avatar Jun 11 '24 18:06 spinylobster