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?
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.
@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!
Julien Puydt has marked this topic as resolved.
Last updated: Dec 07 2023 at 09:01 UTC