Zulip Chat Archive

Stream: general

Topic: equatilies

Patrick Massot (Sep 28 2019 at 07:41):

I just learned a new error message: cases tactic failed, unexpected failure when introducing auxiliary equatilies.

Patrick Massot (Sep 28 2019 at 07:43):

Just in case @Rob Lewis or @Simon Hudon or @Floris van Doorn has a rainy week-end: it would be nice to have a tactic generating extensionality lemmas by throwing away all Props from a structure.

Kevin Buzzard (Sep 28 2019 at 11:46):

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/subtype.20question/near/166990648 :-)

Last updated: Dec 20 2023 at 11:08 UTC