So is the recommended way to use reals with MathComp to require-import reals
from Analysis and do:
Variable R : realType.
or directly use R type from stdlib? or something else?
In Rstruct.v, R is endowed with a realType structure.
So realType lemmas should be usable with R.
indeed both approaches (R-from-stdlib-with-realType vs abstract-realType) are possible/feasible, but what are the tradeoffs? For example, with reals
/realType
, isn't it easier to use the bool comparison operators?
in both cases bool comparison operators are available I think; tradeoffs may depend on your application: thanks to the hierarchy below realType you can state lemmas with the right abstract type but you might also lose field/lra tactics on the other hand (as of today)
Last updated: Feb 05 2023 at 08:28 UTC