I'm stuck on something probably really stupid: `-->`

isn't available after `From mathcomp.analysis Require Import topology sequences`

.

My complete file is:

```
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.analysis Require Import topology sequences.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Scope ring_scope.
Section First.
Variable RR: realFieldType.
Variable r: RR.
Lemma geom_infty: (r > 1) -> (geometric 1 r) --> +oo.
Proof.
Qed.
End First.
```

This notation is in the scope `classical_set_scope`

. This can be observed by looking at its definition in `topology.v`

.

so maybe `Require Import classical_sets`

and open scope, but then you may also need `Require Import normedtype`

and `Import numFieldNormedType.Exports`

to type check the `--> +oo`

notation.

Ah, that's better, but I'm still not there yet: now `geometric 1 r`

and `+oo`

and `-->`

are recognized, but the types don't match!

```
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.analysis Require Import normedtype topology sequences.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Scope classical_set_scope.
Open Scope ring_scope.
Section First.
Variable RR: realFieldType.
Variable r: RR.
Lemma geom_infty: (r > 1) -> (geometric 1 r) --> +oo.
Proof.
Qed.
End First.
```

(deleted)

What do you mean by "requires realType"? As far as I understand, that's what I have and the error message isn't about +oo but about geometric:

```
In environment
RR : realFieldType
r : RR
The term "Phantom (RR) ^nat (geometric 1 r)" has type
"phantom (sequence (GRing.Field.sort (Num.RealField.fieldType RR)))
(@geometric (Num.RealField.fieldType RR)
(GRing.one (GRing.Field.ringType (Num.RealField.fieldType RR))) r)"
while it is expected to have type "phantom (@Filtered.sort ?X ?fX) ?x".
```

I mean it should be `RR: realType`

not `RR: realFieldType`

. `realFieldType`

does not even have filteredtype struture, so you cannot use topological reasoning like `--> +oo`

.

Plus, IIRC `+oo`

is defined for `realType`

only.

EDIT: it was defined for `realFieldType`

, sorry for misdirection.

@abab9579 Changing to `RR: realType`

means I also have to require import `reals`

, but doesn't solve the problem. I posted my whole file to show the problem ; if you have a solution, can you also post it in full?

As @Reynald Affeldt pointed out there were a few missing imports (namely`classical_sets`

and `numFieldNormedType.Exports`

) to make it work:

```
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import boolp classical_sets.
From mathcomp Require Import normedtype topology sequences.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Scope classical_set_scope.
Open Scope ring_scope.
Import numFieldNormedType.Exports.
Section First.
Variable RR: realFieldType.
Variable r: RR.
Lemma geom_infty: (r > 1) -> (geometric 1 r) --> +oo.
Proof.
Qed.
End First.
```

@Cyril Cohen Ah, I was missing the `Import numFieldNormedType.Exports`

, now the sentence makes sense. Thanks!

Julien Puydt has marked this topic as resolved.

Last updated: Jun 22 2024 at 16:02 UTC