## Stream: general

### Topic: docs#conv.interactive.for squashes errors

#### Eric Wieser (Oct 08 2020 at 15:04):

This example succeeds with no diagnostics:

import algebra.ring

example {α : Type*} [ring α] {a b c : α} : (a * b) * c = (a * b) * c :=  begin
conv {
for (_ * _) [1] {
rw add_mul,  -- no error message?
},
},
refl,
end


because docs#conv.interactive.for is implemented in terms of docs#tactic.ext_simplify_core, and ext_simplify_core discards all monadic errors in its pre callback.

#### Eric Wieser (Oct 08 2020 at 15:04):

(https://leanprover-community.github.io/mathlib_docs/tactics.html#conv:%20for, since the link above doesn't go there)

#### Eric Wieser (Oct 08 2020 at 16:07):

I think I know how to fix this, but to do it I need some way to convert a tactic unit into a tactic_result unit, and I don't know enough about monads

#### Eric Wieser (Oct 08 2020 at 16:11):

Specifically, I want the lean equivalent of the python:

try:
new_e, pr =  c.convert e r
except Exception as e:
return (e, ...)  # how do I get e here?
else:
return (None, ...)


#### Eric Wieser (Oct 08 2020 at 16:54):

Worked it out: https://github.com/leanprover-community/lean/pull/476

#### Eric Wieser (Oct 09 2020 at 11:44):

The docs#conv.interactive.find command has a similar problem, where an incorrect "pattern was not found" message is emitted

Last updated: May 14 2021 at 04:22 UTC