Stream: math-comp analysis

Topic: Is `realType` not a `numDomainType`?


view this post on Zulip abab9579 (Aug 19 2022 at 01:20):

I guess this happens because I am returning to Coq after months of hiatus, but I am getting some seemingly strange error.

Basically, I imported normedType and reals files, and typed
Context {V: normedModType realType}
inside a section.
It fails with error which seemingly tells that realType is not a ssrnum.Num.NumDomain.Sort, which I guess is numDomainType.

This does not make sense to me, because reals.v defines canonical numDomainType for the realType. What is happening, which trivial detail am I missing here?

view this post on Zulip Reynald Affeldt (Aug 19 2022 at 01:41):

Maybe try Context {R : realType} {V : normedModType R}.

view this post on Zulip abab9579 (Aug 19 2022 at 01:52):

Ouch, what a gotcha. Thank you again!


Last updated: Feb 05 2023 at 13:02 UTC