------------------------------------------------------------------------
-- The Agda standard library
--
-- Floats
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Float where

open import Data.String.Base using (String)

------------------------------------------------------------------------
-- Re-export built-ins publically

open import Agda.Builtin.Float public
  using
  ( Float
  ; primFloatEquality
  ; primShowFloat
  )

------------------------------------------------------------------------
-- Operations

show : Float → String
show = primShowFloat