mirror of
https://github.com/alecthomas/chroma.git
synced 2025-02-15 13:33:12 +02:00
13 lines
343 B
Plaintext
13 lines
343 B
Plaintext
|
module hello-world where
|
||
|
|
|
||
|
|
open import Agda.Builtin.IO using (IO)
|
||
|
|
open import Agda.Builtin.Unit using (⊤)
|
||
|
|
open import Agda.Builtin.String using (String)
|
||
|
|
|
||
|
|
postulate putStrLn : String → IO ⊤
|
||
|
|
{-# FOREIGN GHC import qualified Data.Text as T #-}
|
||
|
|
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}
|
||
|
|
|
||
|
|
main : IO ⊤
|
||
|
|
main = putStrLn "Hello world!"
|