Zulip Chat Archive

Stream: general

Topic: docs#conv.interactive.for squashes errors


view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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, ...)

view this post on Zulip Eric Wieser (Oct 08 2020 at 16:54):

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

view this post on Zulip 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