mathport:instExpected

Stream: lean4

[Daniel Selsam]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Daniel Selsam]

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]

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

[Mario Carneiro]

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