Commit 2022-09-20 07:09 560891c4View on Github →
⊔ computable on reals (#16463)
This also makes
dist computable on
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.