how do I construct an actual
Everything I read just uses under a
Context trick to assume that such a
t exists as a hypothesis.
what "actual t" means is probably debatable, but the instantiation of realType is all in https://github.com/math-comp/analysis/blob/master/theories/Rstruct.v using reals from the Stdlib.
this might be useful to understand Stdlib reals: https://stackoverflow.com/questions/69683736/real-numbers-in-coq
it might be possible to instantiate realType with CoRN reals (https://github.com/coq-community/corn), but with usual locking protocols, not sure much would be gained...
oh interesting, thanks!
Last updated: Nov 29 2023 at 19:01 UTC