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.

view this post on Zulip 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!

view this post on Zulip Notification Bot (Oct 17 2022 at 06:56):

Julien Puydt has marked this topic as resolved.

Last updated: Jun 25 2024 at 18:02 UTC