module Prim.Data.Float where
Primitive: IEEE754 floatsπ
Yes.
postulate Float : Type {-# BUILTIN FLOAT Float #-} primitive -- Relations primFloatInequality : Float β Float β Bool primFloatEquality : Float β Float β Bool primFloatLess : Float β Float β Bool primFloatIsInfinite : Float β Bool primFloatIsNaN : Float β Bool primFloatIsNegativeZero : Float β Bool primFloatIsSafeInteger : Float β Bool -- Conversions primFloatToWord64 : Float β Maybe Word64 primNatToFloat : Nat β Float primIntToFloat : Int β Float primFloatRound : Float β Maybe Int primFloatFloor : Float β Maybe Int primFloatCeiling : Float β Maybe Int primFloatToRatio : Float β (Ξ£ Int Ξ» _ β Int) primRatioToFloat : Int β Int β Float primFloatDecode : Float β Maybe (Ξ£ Int Ξ» _ β Int) primFloatEncode : Int β Int β Maybe Float primShowFloat : Float β String -- Operations primFloatPlus : Float β Float β Float primFloatMinus : Float β Float β Float primFloatTimes : Float β Float β Float primFloatDiv : Float β Float β Float primFloatPow : Float β Float β Float primFloatNegate : Float β Float primFloatSqrt : Float β Float primFloatExp : Float β Float primFloatLog : Float β Float primFloatSin : Float β Float primFloatCos : Float β Float primFloatTan : Float β Float primFloatASin : Float β Float primFloatACos : Float β Float primFloatATan : Float β Float primFloatATan2 : Float β Float β Float primFloatSinh : Float β Float primFloatCosh : Float β Float primFloatTanh : Float β Float primFloatASinh : Float β Float primFloatACosh : Float β Float primFloatATanh : Float β Float