3 ms·

I think that's necessary, since the order on the full set of reals isn't constructively decideable, so min isn't even a total function there.

• lmm 7y ago
  Almost all reals are not computable, but as far as I know min is total - given two reals (represented as e.g. lazy infinite decimal sequences), computing their min is trivial.
  • leni536 7y ago
    Unless when they happen to be equal. Then it never halts.
    • Skeime 7y ago
      Actually, computing the minimum should work: If they are equal you can still lazily produce the digits of the decimal expansion. What you can’t do in this case is to tell whether this minimum is equal to the first or the second number.
  • JadeNB 7y ago
    Yes, I'm wrong. I was thinking of the naïve implementation if ( a < b ) then { return b } else { return a } which requires being able to decide order, but, as child comments point out, that's not necessary.