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
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: Mar 03 2024 at 16:02 UTC