Commit 2021-10-23 20:04 fc3c0560
View on Github →chore(data/real): make more instances on real, nnreal, and ennreal computable (#9806)
This makes it possible to talk about the add_monoid structure of nnreal and ennreal without worrying about computability.
To make it clear exactly which operations are computable, we remove noncomputable theory.