mirror of
https://github.com/alecthomas/chroma.git
synced 2025-02-05 13:05:18 +02:00
80 lines
3.2 KiB
Plaintext
80 lines
3.2 KiB
Plaintext
[
|
|
{"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"}
|
|
]
|