Zulip Chat Archive

Stream: PR reviews

Topic: lean#476 conv mode find and for


view this post on Zulip Eric Wieser (Oct 12 2020 at 09:52):

The find and for tactics in conv mode (and therefore also conv in ... {}) all throw away error messages, which is a very frustrating experience for me.

I've a fix at lean#476, I'd greatly appreciate if someone could review

view this post on Zulip Eric Wieser (Oct 12 2020 at 09:53):

There was some previous discussion about the PR in https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/instances.20for.20meta.20defs/near/212738421


Last updated: May 06 2021 at 12:15 UTC