New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
wip(data/subtype_instances): introduce closed_under predicate typeclasses #7834
base: master
Are you sure you want to change the base?
Conversation
/-- Typeclass inference can't find this without a large amount of help :(. -/ | ||
example [semiring β] [has_measurable_add₂ β] [has_measurable_mul₂ β]: | ||
semiring (subtype (measurable : (α → β) → Prop)) := | ||
begin | ||
/- `id _` lets us see why typeclass inference is failing. -/ | ||
refine @subtype.closed_under.subtype.semiring _ _ _ (id _) sorry sorry sorry, | ||
convert measurable.subtype.closed_under_zero, | ||
-- uh oh: `mul_zero_class.to_has_zero (α → β) = pi.has_zero` | ||
swap, | ||
apply_instance, | ||
refl, | ||
end |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here's where everything goes wrong
I think you can generalize these to an arbitrary number of inputs with |
That PR looks good and I was already aware of it, but I think that approach would make the typeclass problem worse. |
8fb8837
to
38a5388
Compare
This seemed like it would be a nice generalization, but typeclass inference gets completely stuck in finding these new instances.
This is a more general version of #7833, with the hope of expanding the typeclasses to be used with
submonoid
etc in a future PR.