aboutsummaryrefslogtreecommitdiff
path: root/theories/Floats/FloatAxioms.v
AgeCommit message (Expand)Author
2020-08-09Bring Float notations in line with stdlibJason Gross
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-01Fix ldshiftexpPierre Roux
2019-11-01docs: Add refman+stdlib documentationErik Martin-Dorel
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
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