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
[Merged by Bors] - refactor(data/real/basic): make ⊓
and ⊔
computable on reals
#16463
Conversation
Showing that these coincide with the max and min (respectively) of `real` is left to a follow-up PR. Note that these do not form a `distrib_lattice` as `cau_seq` does not form a `partial_order`.
…ic-wieser/real-computable-min
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
…ic-wieser/real-computable-min
Why is |
Because I didn't want to make this PR grow any further, and had intended to leave that to a followup. My guess would be that it's because |
That feels like good enough justification to rename |
Another option would be to keep |
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.
Thanks 🎉
bors merge
This also makes `norm` and `dist` computable on `real`, `nnreal`, `rat`, and `int`. From a mathematical point of view that doesn't care about computability, this still contains the (mildly) interesting result that the maximum of two reals is equal to the real produced by taking the elementwise maximum of the two cauchy sequences. This change causes some unpleasant elaboration pain in `modular.lean` for reasons presumably linked to unification of dependent typeclasses. It's not clear to me precisely what the cause if. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Pull request successfully merged into master. Build succeeded: |
⊓
and ⊔
computable on reals⊓
and ⊔
computable on reals
This also makes `norm` and `dist` computable on `real`, `nnreal`, `rat`, and `int`. From a mathematical point of view that doesn't care about computability, this still contains the (mildly) interesting result that the maximum of two reals is equal to the real produced by taking the elementwise maximum of the two cauchy sequences. This change causes some unpleasant elaboration pain in `modular.lean` for reasons presumably linked to unification of dependent typeclasses. It's not clear to me precisely what the cause if. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
This also makes
norm
anddist
computable onreal
,nnreal
,rat
, andint
.From a mathematical point of view that doesn't care about computability, this still contains the (mildly) interesting result that the maximum of two reals is equal to the real produced by taking the elementwise maximum of the two cauchy sequences.
This change causes some unpleasant elaboration pain in
modular.lean
for reasons presumably linked to unification of dependent typeclasses. It's not clear to me precisely what the cause if.min
,max
, andabs
#16485distrib_lattice
instance #16493noncomputable theory
withnoncomputable
#16552If the unification issues are particular cause for concern, then I could try to bisect to find which change is responsible.