Zulip Chat Archive

Stream: lean4

Topic: mathport:instExpected


view this post on Zulip Daniel Selsam (Mar 20 2021 at 22:40):

instExpected means a subgoal encountered during search is not known to be a class (since currently lean4 only unfolds reducibles in this context)

@Mario Carneiro do you want to backport this change or just add the one-character patch (one whnf becomes a whnfD) to the fork? The possible downside of the patch is that one might prefer a fast error rather than try whnfD, which could be expensive.

view this post on Zulip Mario Carneiro (Mar 20 2021 at 22:41):

I'm not sure what the source of these errors is. Do you have an example?

view this post on Zulip Mario Carneiro (Mar 20 2021 at 22:42):

it seems odd that typeclass inference would involve an expression that isn't manifestly a class

view this post on Zulip Mario Carneiro (Mar 20 2021 at 22:42):

unless we're talking about things like decidable_eq, but those should be reducible

view this post on Zulip Mario Carneiro (Mar 20 2021 at 22:43):

it's possible that there are some pi classes in category theory that are only semireducible, but the @[class] def PR changed them all to newtyped classes

view this post on Zulip Daniel Selsam (Mar 20 2021 at 22:45):

This is related to the @[class] def issue (https://github.com/dselsam/mathport/issues/4#issuecomment-771347723). I know you backported some changes but I didn't know if you finished. I will double-check what caused the error.

view this post on Zulip Daniel Selsam (Mar 20 2021 at 22:53):

Here is one of the instExpected errors: category_theory.limits.has_finite_products C

view this post on Zulip Daniel Selsam (Mar 20 2021 at 22:58):

FWIW I think I do prefer the lean4 behavior of requiring these be reducible. I am only raising the possibility of a patch, not suggesting it. It depends on (a) how expensive the backport is, and (b) which behavior most people actually prefer.

view this post on Zulip Mario Carneiro (Mar 20 2021 at 23:02):

Yes, that one is now a class (https://github.com/leanprover-community/mathlib/pull/6061/files#diff-f8b477275ac401f2be00f8e5e580ff450be67ab3ef28af9f75d17a09a4647883R23-R24)

view this post on Zulip Mario Carneiro (Mar 20 2021 at 23:03):

I don't think there is any good reason to support semireducible pi classes


Last updated: May 18 2021 at 22:15 UTC