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: Jun 22 2024 at 16:02 UTC