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: Oct 13 2024 at 01:02 UTC