Agda-2.3.2.2: test/epic/Prelude/Float.agda

module Prelude.Float where

open import Prelude.String

postulate
  Float : Set
  floatToString : Float  -> String
  stringToFloat : String -> Float

{-# BUILTIN FLOAT Float #-}
{-# COMPILED_EPIC floatToString (f : Float) -> String = floatToStr(f) #-}
{-# COMPILED_EPIC stringToFloat (s : Any) -> Float = strToFloat(s) #-}