how do I construct an actual t
?
Everything I read just uses under a Section
the Parameter
/Variable
/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: Oct 13 2024 at 01:02 UTC