Julien Puydt (Oct 16 2022 at 14:21): 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?
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