aboutsummaryrefslogtreecommitdiff
path: root/theories/Floats/PrimFloat.v
AgeCommit message (Expand)Author
2019-11-01Fix ldshiftexpPierre Roux
2019-11-01docs: Add refman+stdlib documentationErik Martin-Dorel
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
2019-11-01Pretty-printing primitive float constantsErik Martin-Dorel
2019-11-01Parsing primitive float constantsPierre Roux
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
2019-11-01Put axioms on ldshiftexp and frshiftexpGuillaume Bertholon
2019-11-01Add Floats to standard libraryGuillaume Bertholon