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?
Maybe try Context {R : realType} {V : normedModType R}.
Ouch, what a gotcha. Thank you again!
Reynald Affeldt has marked this topic as resolved.
Last updated: Mar 28 2024 at 18:02 UTC