ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.Float

Logically consistent comparison of floating point numbers.

Synopsis

value asFinite
value isPosInf
value isNegInf
value isPosZero
value isNegZero
value isSafeInteger
value doubleEq
value doubleLe
value doubleLt
value intToDouble
value doublePlus
value doubleMinus
value doubleTimes
value doubleNegate
value doubleDiv
value doublePow
value doubleSqrt
value doubleExp
value doubleLog
value doubleSin
value doubleCos
value doubleTan
value doubleASin
value doubleACos
value doubleATan
value doubleATan2
value doubleSinh
value doubleCosh
value doubleTanh
value doubleASinh
value doubleACosh
value doubleATanh
value doubleRound
value doubleFloor
value doubleCeiling
value doubleDenotEq
value doubleDenotOrd
value doubleToWord64
value doubleToRatio
value ratioToDouble
value doubleDecode
value doubleEncode
value toStringWithoutDotZero

PackageAgda-2.8.0.2
Exports43
LanguageHaskell2010
LicenceMIT
SourceFloat.hs

valueasFinite :: Double -> Maybe Double

Source#

Return Just x if it's a finite number, otherwise return Nothing.

valueisPosInf :: Double -> Bool

valueisNegInf :: Double -> Bool

valueisPosZero :: Double -> Bool

valueisNegZero :: Double -> Bool

valueisSafeInteger :: Double -> Bool

Source#

Checks whether or not the Double is within a safe range of operation.

valuedoubleEq :: Double -> Double -> Bool

valuedoubleLe :: Double -> Double -> Bool

valuedoubleLt :: Double -> Double -> Bool

valueintToDouble :: Integral a => a -> Double

valuedoublePlus :: Double -> Double -> Double

valuedoubleMinus :: Double -> Double -> Double

valuedoubleTimes :: Double -> Double -> Double

valuedoubleNegate :: Double -> Double

valuedoubleDiv :: Double -> Double -> Double

valuedoublePow :: Double -> Double -> Double

valuedoubleSqrt :: Double -> Double

valuedoubleExp :: Double -> Double

valuedoubleLog :: Double -> Double

valuedoubleSin :: Double -> Double

valuedoubleCos :: Double -> Double

valuedoubleTan :: Double -> Double

valuedoubleASin :: Double -> Double

valuedoubleACos :: Double -> Double

valuedoubleATan :: Double -> Double

valuedoubleATan2 :: Double -> Double -> Double

valuedoubleSinh :: Double -> Double

valuedoubleCosh :: Double -> Double

valuedoubleTanh :: Double -> Double

valuedoubleASinh :: Double -> Double

valuedoubleACosh :: Double -> Double

valuedoubleATanh :: Double -> Double

valuedoubleRound :: Double -> Maybe Integer

valuedoubleFloor :: Double -> Maybe Integer

valuedoubleCeiling :: Double -> Maybe Integer

valuedoubleDenotEq :: Double -> Double -> Bool

Source#

Denotational equality for floating point numbers, checks bitwise equality.

NOTE: Denotational equality distinguishes NaNs, so its results may vary depending on the architecture and compilation flags. Unfortunately, this is a problem with floating-point numbers in general.

valuedoubleDenotOrd :: Double -> Double -> Ordering

Source#

I guess "denotational orderings" are now a thing? The point is that we need an Ord instance which provides a total ordering, and is consistent with the denotational equality.

NOTE: The ordering induced via doubleToWord64 is total, and is consistent with doubleDenotEq. However, it is *deeply* unintuitive. For one, it considers all negative numbers to be larger than positive numbers.