Stream: math-comp users

Topic: Missing notations with reals?

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

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

view this post on Zulip Julien Puydt (Jun 13 2022 at 06:49):

Excellent, thanks!

Last updated: Jul 25 2024 at 16:02 UTC