nnreal): make `real.to_nnreal` computable

Commit

3 years ago

chore(data/real/nnreal): make `real.to_nnreal` computable `max` is not computable due to the `linear_order` argument, but the defeq `sup` is.

References

Author

eric-wieser

Committer

eric-wieser

Parents