Agda-2.3.2.2: test/Common/MAlonzo.agda

module Common.MAlonzo where

open import Common.Prelude
open import Common.Coinduction

postulate
  putStrLn : ∞ String → IO Unit

{-# COMPILED putStrLn putStrLn #-}

main = putStrLn (♯ "This is a dummy main routine.")

mainPrint : String → _
mainPrint s = putStrLn (♯ s)

postulate
  natToString : Nat → String

{-# COMPILED natToString show #-}

mainPrintNat : Nat → _
mainPrintNat n = putStrLn (♯ (natToString n))