104 lines
2.4 KiB
Text
Generated
104 lines
2.4 KiB
Text
Generated
'\\documentclass' Keyword
|
|
'{' Name.Builtin
|
|
'article' Text
|
|
'}' Name.Builtin
|
|
'\n' Text
|
|
|
|
'% this is a LaTeX comment\n' Comment
|
|
|
|
'\\usepackage' Keyword
|
|
'{' Name.Builtin
|
|
'agda' Text
|
|
'}' Name.Builtin
|
|
'\n\n' Text
|
|
|
|
'\\begin' Keyword
|
|
'{' Name.Builtin
|
|
'document' Text
|
|
'}' Name.Builtin
|
|
"\n\nHere's how you can define " Text
|
|
'\\emph' Keyword
|
|
'{' Name.Builtin
|
|
'RGB' Text
|
|
'}' Name.Builtin
|
|
' colors in Agda:\n\n' Text
|
|
|
|
'\\begin' Keyword
|
|
'{' Name.Builtin
|
|
'code' Text
|
|
'}' Name.Builtin
|
|
'\n' Text
|
|
|
|
'module' Keyword.Reserved
|
|
' ' Text.Whitespace
|
|
'example' Name
|
|
' ' Text.Whitespace
|
|
'where' Keyword.Reserved
|
|
'\n' Text.Whitespace
|
|
|
|
'\n' Text.Whitespace
|
|
|
|
'open' Keyword.Reserved
|
|
' ' Text.Whitespace
|
|
'import' Keyword.Reserved
|
|
' ' Text.Whitespace
|
|
'Data.Fin' Name
|
|
'\n' Text.Whitespace
|
|
|
|
'open' Keyword.Reserved
|
|
' ' Text.Whitespace
|
|
'import' Keyword.Reserved
|
|
' ' Text.Whitespace
|
|
'Data.Nat' Name
|
|
'\n' Text.Whitespace
|
|
|
|
'\n' Text.Whitespace
|
|
|
|
'data' Keyword.Reserved
|
|
' ' Text.Whitespace
|
|
'Color' Text
|
|
' ' Text.Whitespace
|
|
':' Operator.Word
|
|
' ' Text.Whitespace
|
|
'Set' Keyword.Type
|
|
' ' Text.Whitespace
|
|
'where' Keyword.Reserved
|
|
'\n' Text.Whitespace
|
|
|
|
' ' Text.Whitespace
|
|
'RGB' Name.Function
|
|
' ' Text.Whitespace
|
|
':' Operator.Word
|
|
' ' Text.Whitespace
|
|
'Fin' Text
|
|
' ' Text.Whitespace
|
|
'256' Literal.Number.Integer
|
|
' ' Text.Whitespace
|
|
'→' Operator.Word
|
|
' ' Text.Whitespace
|
|
'Fin' Text
|
|
' ' Text.Whitespace
|
|
'256' Literal.Number.Integer
|
|
' ' Text.Whitespace
|
|
'→' Operator.Word
|
|
' ' Text.Whitespace
|
|
'Fin' Text
|
|
' ' Text.Whitespace
|
|
'256' Literal.Number.Integer
|
|
' ' Text.Whitespace
|
|
'→' Operator.Word
|
|
' ' Text.Whitespace
|
|
'Color' Text
|
|
'\n' Text.Whitespace
|
|
|
|
'\\end' Keyword
|
|
'{' Name.Builtin
|
|
'code' Text
|
|
'}' Name.Builtin
|
|
'\n\n' Text
|
|
|
|
'\\end' Keyword
|
|
'{' Name.Builtin
|
|
'document' Text
|
|
'}' Name.Builtin
|
|
'\n' Text
|