I tried a bunch of different requires, scopes, etc., but is it currently at all supported to get the usual infix notations for the boolean versions of the comparison operators on `R`

, like how `ssrnat`

gives you the boolean ones for `nat`

? For example:

```
Variable r1 r2 : R.
Check r1 <= r2.
(*
should show:
r1 <= r2 : bool
as opposed to:
r1 <= r2 : Prop
*)
```

Since I seldom deal directly with Reals in mathcomp-analysis, I have no default recipe but for example the following has type bool:

```
Require Import Rstruct.
Check Rdefinitions.R0 <= Rdefinitions.R1.
(* Rdefinitions.RbaseSymbolsImpl.R0 <= Rdefinitions.RbaseSymbolsImpl.R1
: bool *)
```

Or this:

```
Require Import Rstruct.
Check (0 <= 1 :> Rdefinitions.R).
(* (0 : Rdefinitions.RbaseSymbolsImpl.R) <= (1 : Rdefinitions.RbaseSymbolsImpl.R)
: bool *)
```

Or this:

```
Require Import Reals.
Require Import Rstruct.
Check (0 <= 1 :> R).
(* (0 : R) <= (1 : R)
: bool *)
```

(let's say in a context that Require Import the files up to normedtype.v)

hmm, so like this?

```
From Coq Require Import Reals.
From mathcomp.analysis Require Import
boolp ereal reals posnum landau classical_sets Rstruct Rbar topology prodnormedzmodule normedtype.
(*
this gives using release 0.3.2:
Error:
Level 2 is already declared right associative while it is now expected to be left associative.
*)
```

Maybe insert this in-between:

```
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum.
```

(only the first line is sufficient to get rid of the error)

I may be missing something:

```
From Coq Require Import Reals.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum.
From mathcomp.analysis Require Import
boolp ereal reals posnum landau classical_sets Rstruct Rbar topology prodnormedzmodule normedtype.
Fail Check (0 <= 1 :> Rdefinitions.R). (* Unknown interpretation for notation "_ <= _ :> _". *)
Fail Check (0 <= 1 :> R). (* Unknown interpretation for notation "_ <= _ :> _". *)
```

`Local Open Scope ring_scope.`

before the `Check`

s

(with my apologies: I should have prepared a minimal example from the start but I was not in a working environment)

Last updated: Jun 22 2024 at 15:01 UTC