search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
194 stars 43 forks source link

floor and ceil to be subsumed by MathComp #330

Closed affeldt-aist closed 1 month ago

affeldt-aist commented 3 years ago

TODO: revise the use of floor and ceil once math-comp/math-comp#682 is merged into MathComp requiring MC >= 2.1.0

affeldt-aist commented 3 months ago

From version 1.2.0, we'll support MathComp >= 2.1, so it is about time to make this change. The deprecation warnings have been removed so that now the expressions to be subsumed appear as reals.blah (e.g., reals.floor, reals.ceil, etc. as in https://github.com/math-comp/analysis/blob/master/theories/normedtype.v#L255).