Zulip Chat Archive

Stream: lean4

Topic: mathport:instExpected


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.

Mario Carneiro (Mar 20 2021 at 22:41):

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

Mario Carneiro (Mar 20 2021 at 22:42):

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

Mario Carneiro (Mar 20 2021 at 22:42):

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

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

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.

Daniel Selsam (Mar 20 2021 at 22:53):

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

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.

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)

Mario Carneiro (Mar 20 2021 at 23:03):

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


Last updated: Dec 20 2023 at 11:08 UTC