[
  {"type":"KeywordReserved","value":"module"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hello"},
  {"type":"Text","value":"-world"},
  {"type":"TextWhitespace","value":" "},
  {"type":"KeywordReserved","value":"where"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"KeywordReserved","value":"open"},
  {"type":"TextWhitespace","value":" "},
  {"type":"KeywordReserved","value":"import"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"Agda.Builtin.IO"},
  {"type":"TextWhitespace","value":" "},
  {"type":"KeywordReserved","value":"using"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"("},
  {"type":"Text","value":"IO"},
  {"type":"Operator","value":")"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordReserved","value":"open"},
  {"type":"TextWhitespace","value":" "},
  {"type":"KeywordReserved","value":"import"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"Agda.Builtin.Unit"},
  {"type":"TextWhitespace","value":" "},
  {"type":"KeywordReserved","value":"using"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"("},
  {"type":"Text","value":"⊤"},
  {"type":"Operator","value":")"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordReserved","value":"open"},
  {"type":"TextWhitespace","value":" "},
  {"type":"KeywordReserved","value":"import"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"Agda.Builtin.String"},
  {"type":"TextWhitespace","value":" "},
  {"type":"KeywordReserved","value":"using"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"("},
  {"type":"Text","value":"String"},
  {"type":"Operator","value":")"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"KeywordReserved","value":"postulate"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Text","value":"putStrLn"},
  {"type":"TextWhitespace","value":" "},
  {"type":"OperatorWord","value":":"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Text","value":"String"},
  {"type":"TextWhitespace","value":" "},
  {"type":"OperatorWord","value":"→"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Text","value":"IO"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Text","value":"⊤"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"CommentMultiline","value":"{-# FOREIGN GHC import qualified Data.Text as T #-}"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"CommentMultiline","value":"{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"NameFunction","value":"main"},
  {"type":"TextWhitespace","value":" "},
  {"type":"OperatorWord","value":":"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Text","value":"IO"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Text","value":"⊤"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"Text","value":"main"},
  {"type":"TextWhitespace","value":" "},
  {"type":"OperatorWord","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Text","value":"putStrLn"},
  {"type":"TextWhitespace","value":" "},
  {"type":"LiteralString","value":"\"Hello world!\""},
  {"type":"TextWhitespace","value":"\n"}
]