search

leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
204 stars 47 forks source link

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

Open spinylobster opened 1 month ago

spinylobster commented 1 month ago

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 α.