Zulip Chat Archive
Stream: general
Topic: computable_min
Kenny Lau (Jul 28 2018 at 15:51):
I think we should have a typeclass computable_min
Kenny Lau (Jul 28 2018 at 15:52):
e.g. the real numbers have computable min although not having discrete linear order
Chris Hughes (Jul 28 2018 at 17:00):
What's the use of computable min on reals, when you can't really do anything with a computable real?
Last updated: May 02 2025 at 03:31 UTC