-- Adapted from test/Compiler/simple/HelloWorld.agda in the maint branch.

-- Tested with Agda 2.4.2.5.

module HelloWorld where

data Unit : Set where
  unit : Unit

{-# COMPILED_DATA Unit () () #-}

data List A : Set where
  []  : List A
  _∷_ : A → List A → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _∷_  #-}

postulate
  String : Set

{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE String String #-}

postulate
  IO : Set → Set

{-# BUILTIN IO IO #-}
{-# COMPILED_TYPE IO IO #-}

postulate
  putStr : String → IO Unit

{-# COMPILED putStr putStr #-}

main : IO Unit
main = putStr "Hello World"