Stream: math-comp analysis

Topic: `\bar R` as more than Set?

view this post on Zulip Julien Puydt (Oct 16 2022 at 14:21):

I was making yet another experiment, and got stuck because I'm using \bar R, which is seen as a Set, while I would need it to be an eqType, and soon also an orderType. I think the R I use is the one you get from Require Import Reals... it does matter, doesn't it?

view this post on Zulip Cyril Cohen (Oct 16 2022 at 18:34):

It should not matter which R you're using as long as it has enough canonical instances. Now, the one from Reals must be used in conjunction with Rstruct, which declares all the necessary canonical instances.

Last updated: Feb 05 2023 at 14:02 UTC