80 lines
3.2 KiB
Text
80 lines
3.2 KiB
Text
|
[
|
|||
|
|
{"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"}
|
|||
|
|
]
|