Julien Puydt (Jun 13 2022 at 06:32): Julien Puydt (Jun 13 2022 at 06:32):With bare Coq, one can do:
Require Import Reals.
Open Scope R_scope.
Check 1 / 3.
which makes it pretty convenient to work with.
But if I try to do the same using mathcomp's reals:
From mathcomp.analysis Require Import reals.
Open Scope real_scope.
Fail Check 1 / 3.
Of course, I can do:
From mathcomp Require Import ssralg.
Open Scope ring_scope.
Check 1 / 3%:R.
but while not completely painful, it's pretty unfriendly.
I'm not quite sure where the relevant notations should be added - I don't know enough yet to do it, but I'm willing to learn...
(putting it in the math-comp users channel because there's a change I missed something, but might migrate to math-comp devs if it's indeed an issue)
Pierre Roux (Jun 13 2022 at 06:47):1 / 3%:R (or / 3%:R or 3%:R^-1) is the expected syntax currently. 1 / 3 will be equivalent in the next release (to be available soon hopefully to support Coq 8.16)
Julien Puydt (Jun 13 2022 at 06:49):Excellent, thanks!
Last updated: Oct 13 2024 at 01:02 UTC