Contents

For Agda 2.6.2, based on its [https://agda.readthedocs.io/en/v2.6.2/getting-started/hello-world.html documentation].
module helloworld where

open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit renaming (⊤ to Unit)
open import Agda.Builtin.String using (String)

postulate putStrLn : String -> IO Unit
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}

main : IO Unit
main = putStrLn "Hello world!"

Version data entries

10 entries across 7 versions & 1 rubygems

Version	Path
zettacode-0.1.7	files.zettacode/hello_world.text/agda.txt
zettacode-0.1.6	files.zettacode/hello_world.text/agda.txt
zettacode-0.1.6	files.zettacode2/hello_world.text/agda.txt
zettacode-0.1.5	files.zettacode/hello_world.text/agda.txt
zettacode-0.1.5	files.zettacode2/hello_world.text/agda.txt
zettacode-0.1.4	files.zettacode/hello_world.text/agda.txt
zettacode-0.1.4	files.zettacode2/hello_world.text/agda.txt
zettacode-0.1.3	files.zettacode/hello_world.text/agda.txt
zettacode-0.1.2	files.zettacode/hello_world.text/agda.txt
zettacode-0.1.1	zettacode.files/hello_world.text/agda.txt