is_R_or_C universe

Stream: general

[Sebastien Gouezel]

We have a predicate is_R_or_C, which will only ever be satisfied by $\R$ and $\mathbb{C}$. Currently, it is defined as a predicate on k : Type*. Since it will only ever be used for fields in Type, is there a harm to restricting it to a predicate on Type? Can it help unification somewhat, or on the contrary could this create problems?

[Johan Commelin]

It might be applied to the completion of a number field at an infinite prime. This means that all those applications in number theory will be restricted to Type. Not a mathematical problem... but we need to keep such things in mind.

[Sebastien Gouezel]

Hmm, yes, good point, it also applies to unusual copies of the reals.