79 lines
3.2 KiB
Text
79 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"}
|
||
]
|