realType not inheriting orderTopologicalType from realFieldType #1800
Description
realFieldType implements the interface orderTopologicalType, but realType does not inherit it. Example shows use of lemma that requires orderTopologicalType
From mathcomp Require Import all_ssreflect all_algebra all_analysis all_reals all_classical.
Import Num.Theory GRing.Theory Order.POrderTheory.
Import numFieldNormedType.Exports.
Import numFieldTopology.Exports.
Open Scope ring_scope.
Open Scope order_scope.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Lemma example (R : realType) (R' : realFieldType) : True.
Proof.
have := @max_fun_continuous _ _ R'.
have := @max_fun_continuous _ _ R.The first have statement is accepted, where it expects R' : orderTopologicalType, but the second expects R : orderTopologicalType and this does not work.