Stream: math-comp analysis

Topic: an actual `t : realType`


view this post on Zulip Quinn (Nov 10 2022 at 19:22):

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.

view this post on Zulip Karl Palmskog (Nov 11 2022 at 09:56):

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.

view this post on Zulip Karl Palmskog (Nov 11 2022 at 09:57):

this might be useful to understand Stdlib reals: https://stackoverflow.com/questions/69683736/real-numbers-in-coq

view this post on Zulip Karl Palmskog (Nov 11 2022 at 10:03):

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...

view this post on Zulip Quinn (Nov 11 2022 at 12:31):

oh interesting, thanks!


Last updated: Jan 30 2023 at 12:03 UTC