erased reals

Stream: general

[Reid Barton]

Have we ever considered forcing the reals to be "computable" by using erased? If we are making them irreducible anyways then this should be sort of okay to do, right?

[Gabriel Ebner]

I have definitely considered it and approve of the change.

[Eric Wieser]

Right now reals are actually computable up until you do division or order comparisons, right?

[Eric Wieser]

You can actually ask the VM to give you a cauchy sequence?

[Johan Commelin]

What are the benefits of doing this? Just that we don't need to write noncomputable so often? Or are there other benefits?

[Reid Barton]

Yeah, exactly that

[Reid Barton]

Well but then there are knock-on benefits as well, as Eric discovered in the topic about noncomputable instances

[Reid Barton]

Stuff we actually want to compute won't get tainted by appearing in the same instance declaration as stuff that can't be computed