Hello, World! in Agda
Just writing strings is not a natural task for Agda, so it needs some extra installations.
This example should be saved in file “helloworld.agda”. You’ll have to install agda standard library (agda-stdlib); this was tested with agda 2.2.6 and agda-stdlib 0.3. To compile the example, use
agda -i [library path] -i . -c helloworld.agda, where
[library path] is a path to where you installed agda-stdlib. This compiles Agda source code into Haskell code, and then converts it into an executable.
module helloworld where open import IO.Primitive using (IO; putStrLn) open import Data.String using (toCostring; String) open import Data.Char using (Char) open import Foreign.Haskell using (fromColist; Colist; Unit) open import Data.Function fromString = fromColist . toCostring main : IO Unit main = putStrLn (fromString "Hello, World!")