Stream: math-comp analysis

Topic: ✔ `\bar R` as more than Set?

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: Feb 05 2023 at 14:02 UTC