packages feed

Agda-2.3.2.2: examples/outdated-and-incorrect/Alonzo/RTP.hs.sav

module RTP where
import qualified Prelude
-- import qualified RTS

undefined = Prelude.undefined
data Bool = False | True

type Float = Prelude.Double
-- newtype Float = FloatT { unboxFloat :: Prelude.Float}
newtype Char = CharT { unboxChar :: Prelude.Char }

_Int = ()
_Float = ()
_String =  ()
_Char = ()

_primShowBool :: Bool -> Prelude.String
_primShowBool False = "False"
_primShowBool True = "True"

_primShowInt :: Prelude.Int -> Prelude.String
_primShowInt = Prelude.show

_primIntZero :: Prelude.Int 
_primIntZero = (0::Prelude.Int)

_primIntOne :: Prelude.Int 
_primIntOne = (1::Prelude.Int)

_primShowFloat :: Float -> Prelude.String
_primShowFloat f = Prelude.show f
-- _primShowFloat (FloatT f) = Prelude.show f

_primShowChar c = [ unboxChar c]

_primStringAppend :: Prelude.String -> Prelude.String -> Prelude.String
_primStringAppend = (Prelude.++)

_primStringReverse = Prelude.reverse
_primStringToList s = Prelude.map CharT s
_primStringFromList s = Prelude.map unboxChar s

_primNatPlus = undefined
_primNatMinus = undefined
_primNatTimes = undefined
_primNatDivSuc = undefined
_primNatModSuc = undefined
_primNatLess = undefined
_primNatEquals = undefined