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.
Julien Puydt (Oct 17 2022 at 06:56):@Cyril Cohen Ah, perhaps that's what was blocking me... but I started to move my experiment away from Coq's Reals to MC-analysis' reals so I can't check anymore... I'll know if that works when I'll have fixed my other eqType issues... thanks!
Notification Bot (Oct 17 2022 at 06:56):Julien Puydt has marked this topic as resolved.
Last updated: Dec 07 2023 at 09:01 UTC