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