Skip to content

Instantly share code, notes, and snippets.

@Hagb
Last active April 22, 2023 11:34
Show Gist options
  • Save Hagb/df9044a81525aff0f6b44f4fae3270c0 to your computer and use it in GitHub Desktop.
Save Hagb/df9044a81525aff0f6b44f4fae3270c0 to your computer and use it in GitHub Desktop.
KDE Syntax Highlighting XML file for Lean
<?xml version="1.0" encoding="UTF-8"?>
<!--
based on pygments highlighting file for Lean4 (https://github.com/leanprover/lean4/blob/master/doc/latex/lean4.py)
and VSCode highlighting file for Lean4 (https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/syntaxes/lean4.json).
-->
<language name="Lean" version="1" kateversion="2.4" section="Sources" extensions="*.lean;*.lean4"
mimetype="text/x-lean">
<highlighting>
<!-- {
"name": "Lean 4",
"scopeName": "source.lean4",
"fileTypes": [],
"patterns": [-->
<!-- TODO { "include": "#comments" }, -->
<!-- { "match": "\\b(Prop|Type|Sort)\\b", "name": "storage.type.lean4" }, -->
<list name="Types"> <!-- dsBuiltIn -->
<item>Prop</item>
<item>Type</item>
<item>Sort</item>
</list>
<!-- { "match": "\\battribute\\b\\s*\\[[^\\]]*\\]", "name": "storage.modifier.lean4" }, -->
<list name="attribute"> <!-- dsAttribute -->
<item>attribute</item>
</list>
<!-- { "match": "@\\[[^\\]]*\\]", "name": "storage.modifier.lean4" },-->
<!--{
"match":
"\\b(?<!\\.)(global|local|scoped|partial|unsafe|private|protected|noncomputable)(?!\\.)\\b",
"name": "storage.modifier.lean4"
}, -->
<list name="Modifiers"> <!-- dsAttribute -->
<item>global</item>
<item>local</item>
<item>scoped</item>
<item>partial</item>
<item>unsafe</item>
<item>private</item>
<item>protected</item>
<item>noncomputable</item>
</list>
<!-- { "match": "\\bsorry\\b", "name": "invalid.illegal.lean4" }, -->
<list name="sorry"> <!-- dsWarning -->
<item>sorry</item>
<item>admit</item>
</list>
<!-- { "match": "#(print|eval|reduce|check|check_failure)\\b", "name": "keyword.other.lean4"
}, -->
<list name="Commands"> <!-- dsPreprocessor -->
<item>#print</item>
<item>#eval</item>
<item>#reduce</item>
<item>#check</item>
<item>#check_failure</item>
<item>#align</item>
</list>
<!-- TODO {
"match": "\\bderiving\\s+instance\\b",
"name": "keyword.other.command.lean4"
}, -->
<!-- {
"begin":
"\\b(?<!\\.)(inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class|constant)\\b\\s+(\\{[^}]*\\})?",
"beginCaptures": {
"1": {"name": "keyword.other.definitioncommand.lean4"}
},
"patterns": [
{"include": "#comments"},
{"include": "#definitionName"},
{"match": ","}
],
"end": "(?=\\bwith\\b|\\bextends\\b|\\bwhere\\b|[:\\|\\(\\[\\{⦃<>])",
"name": "meta.definitioncommand.lean4"
}, -->
<list name="Definitions"> <!-- dsKeyword --> <!-- dsFunction until with -->
<item>inductive</item>
<item>coinductive</item>
<item>structure</item>
<item>theorem</item>
<item>axiom</item>
<item>abbrev</item>
<item>lemma</item>
<item>def</item>
<item>instance</item>
<item>class</item>
<item>constant</item>
</list>
<list name="DefinitionsAfterName">
<item>with</item>
<item>extends</item>
<item>where</item>
<!-- <item>:</item>
<item>|</item>
<item>(</item>
<item>[</item>
<item>{</item>
<item>⦃</item>
<item><</item>
<item>></item> -->
</list>
<!-- {
"match":
"\\b(?<!\\.)(theorem|show|have|from|suffices|nomatch|def|class|structure|instance|set_option|initialize|builtin_initialize|example|inductive|coinductive|axiom|constant|universe|universes|variable|variables|import|open|export|theory|prelude|renaming|hiding|exposing|do|by|let|extends|mutual|mut|where|rec|syntax|macro_rules|macro|deriving|fun|section|namespace|end|infix|infixl|infixr|postfix|prefix|notation|abbrev|if|then|else|calc|match|with|for|in|unless|try|catch|finally|return|continue|break)(?!\\.)\\b",
"name": "keyword.other.lean4"
}, -->
<list name="import"> <!-- dsImport -->
<item>import</item>
</list>
<list name="ControlFlows"> <!-- dsControlFlow -->
<item>if</item>
<item>then</item>
<item>else</item>
<item>calc</item>
<item>match</item>
<item>try</item>
<item>catch</item>
<item>finally</item>
<item>return</item>
<item>continue</item>
<item>break</item>
<item>for</item>
<item>do</item>
</list>
<list name="Keywords"> <!-- dsKeyword -->
<item>theorem</item>
<item>def</item>
<item>class</item>
<item>axiom</item>
<item>constant</item>
<item>universe</item>
<item>universes</item>
<item>variable</item>
<item>variables</item>
<item>example</item>
<item>structure</item>
<item>instance</item>
<item>postfix</item>
<item>prefix</item>
<item>notation</item>
<item>abbrev</item>
<item>infix</item>
<item>infixl</item>
<item>infixr</item>
<item>show</item>
<item>have</item>
<item>from</item>
<item>suffices</item>
<item>nomatch</item>
<item>set_option</item>
<item>initialize</item>
<item>builtin_initialize</item>
<item>inductive</item>
<item>coinductive</item>
<item>open</item>
<item>export</item>
<item>theory</item>
<item>prelude</item>
<item>renaming</item>
<item>hiding</item>
<item>exposing</item>
<item>by</item>
<item>let</item>
<item>extends</item>
<item>mutual</item>
<item>mut</item>
<item>where</item>
<item>rec</item>
<item>syntax</item>
<item>macro_rules</item>
<item>macro</item>
<item>deriving</item>
<item>fun</item>
<item>section</item>
<item>namespace</item>
<item>end</item>
<item>with</item>
<item>in</item>
<item>unless</item>
<item>at</item>
<item>use</item>
<item>begin</item>
</list>
<list name="Tactics">
<item>intro</item>
<item>intros</item>
<item>rename</item>
<item>revert</item>
<item>clear</item>
<item>subst</item>
<item>subst_vars</item>
<item>assumption</item>
<item>contradiction</item>
<item>apply</item>
<item>exact</item>
<item>refine</item>
<item>refine'</item>
<item>constructor</item>
<item>case</item>
<item>case'</item>
<item>all_goals</item>
<item>any_goals</item>
<item>trace</item>
<item>first</item>
<item>rotate_left</item>
<item>rotate_right</item>
<item>try</item>
<item>rfl</item>
<item>rfl'</item>
<item>ac_rfl</item>
<item>sorry</item>
<item>admit</item>
<item>infer_instance</item>
<item>change</item>
<item>rewrite</item>
<item>rw</item>
<item>injection</item>
<item>injections</item>
<item>simp</item>
<item>simp_all</item>
<item>dsimp</item>
<item>delta</item>
<item>unfold</item>
<item>refine_lift</item>
<item>have</item>
<item>suffices</item>
<item>let</item>
<item>show</item>
<item>refine_lift'</item>
<item>have'</item>
<item>let'</item>
<item>induction</item>
<item>generalize</item>
<item>cases</item>
<item>rename_i</item>
<item>repeat</item>
<item>trivial</item>
<item>split</item>
<item>stop</item>
<item>specialize</item>
<item>unhygienic</item>
<item>fail</item>
<item>checkpoint</item>
<item>save</item>
<item>sleep</item>
<item>exists</item>
<item>congr</item>
<item>simp</item>
<item>introv</item>
<item>transitivity</item>
<item>use</item>
<item>inductive'</item>
<item>rcases</item>
<item>obtain</item>
<item>by_cases</item>
<item>simpa</item>
<item>cases'</item>
<item>contrapose!</item>
<item>contrapose</item>
<item>rwa</item>
<item>ext</item>
<item>push_neg</item>
<item>nth_rw</item>
<item>by_contra</item>
<item>by_contra'</item>
<item>conv_rhs</item>
<item>conv_lhs</item>
<item>linarith</item>
<item>library_search</item>
<item>rintro</item>
<item>rintros</item>
<item>choose</item>
<item>ring</item>
<item>exfalso</item>
<item>by_contradiction</item>
<item>by_contradiction'</item>
<item>left</item>
<item>right</item>
<item>refl</item>
<item>from</item>
<item>using</item>
</list>
<!-- { "begin": "«", "end": "»", "contentName": "entity.name.lean4" }, -->
<!-- {
"begin": "\"", "end": "\"",
"name": "string.quoted.double.lean4",
"patterns": [
{ "match": "\\\\[\\\\\"ntr']", "name": "constant.character.escape.lean4" },
{ "match": "\\\\x[0-9A-Fa-f][0-9A-Fa-f]", "name": "constant.character.escape.lean4" },
{ "match": "\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]", "name":
"constant.character.escape.lean4" }
]
}, -->
<!-- { "name": "constant.language.lean4", "match": "\\b(true|false)\\b" }, -->
<list name="Constants"> <!-- dsConstant -->
<item>true</item>
<item>false</item>
</list>
<!-- TODO { "name": "string.quoted.single.lean4", "match": "'[^\\\\']'" },
{ "name": "string.quoted.single.lean4", "match":
"'(\\\\(x[0-9A-Fa-f][0-9A-Fa-f]|u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]|.))'",
"captures": { "1": { "name": "constant.character.escape.lean4" } } },
{ "match": "`+[^\\[(]\\S+", "name": "entity.name.lean4" },-->
<!-- { "match":
"\\b([0-9]+|0([xX][0-9a-fA-F]+)|[-]?(0|[1-9][0-9]*)(\\.[0-9]+)?([eE][+-]?[0-9]+)?)\\b",
"name": "constant.numeric.lean4" } -->
<!-- ], -->
<!--"repository":
{
"definitionName": {
"patterns": [
{"match": "\\b[^:«»\\(\\)\\{\\}[:space:]=→λ∀?][^:«»\\(\\)\\{\\}[:space:]]*", "name":
"entity.name.function.lean4"},
{"begin": "«", "end": "»", "contentName": "entity.name.function.lean4"}
]
},
"dashComment": {
"begin": "--><!--", "end": "$",
"name": "comment.line.double-dash.lean4",
"patterns": [
{ "include": "source.lean.markdown" }
]
},
"docComment": {
"begin": "/--><!--", "end": "-/", "name": "comment.block.documentation.lean4",
"patterns": [
{ "include": "source.lean.markdown" },
{ "include": "#blockComment" }
]
},
"modDocComment": {
"begin": "/-!", "end": "-/", "name": "comment.block.documentation.lean4",
"patterns": [
{ "include": "source.lean.markdown" },
{ "include": "#blockComment" }
]
},
"blockComment": {
"begin": "/-", "end": "-/", "name": "comment.block.lean4",
"patterns": [
{ "include": "source.lean.markdown" },
{ "include": "#blockComment" }
]
},
"comments": {
"patterns": [
{ "include": "#dashComment" },
{ "include": "#docComment" },
{ "include": "#stringBlock" },
{ "include": "#modDocComment" },
{ "include": "#blockComment" }
]
}
}
} -->
<contexts>
<context attribute="Normal Text" lineEndContext="#stay" name="Normal Text">
<keyword attribute="Types" context="#stay" String="Types" />
<keyword attribute="Modifiers" context="#stay" String="Modifiers" />
<RegExpr attribute="Modifiers" context="#stay" String="(?:attribute\b\s*|@)\[[^\]]*\]" />
<keyword attribute="sorry" context="#stay" String="sorry" />
<keyword attribute="Commands" context="#stay" String="Commands" />
<keyword attribute="import" context="Importing" String="import" />
<keyword attribute="ControlFlows" context="#stay" String="ControlFlows" />
<keyword attribute="Definitions" context="defining" String="Definitions" />
<keyword attribute="Tactics" context="#stay" String="Tactics" />
<keyword attribute="Keywords" context="#stay" String="Keywords" />
<keyword attribute="Constants" context="#stay" String="Constants" />
<RangeDetect attribute="NameEscape" context="#stay" char="«" char1="»" />
<RegExpr attribute="Name" context="#stay"
String="[A-Za-z_&#x03b1;-&#x03ba;&#x03bc;-&#x03fb;&#x1f00;-&#x1ffe;&#x2100;-&#x214f;][A-Za-z_'&#x03b1;-&#x03ba;&#x03bc;-&#x03fb;&#x1f00;-&#x1ffe;&#x2070;-&#x2079;&#x207f;-&#x2089;&#x2090;-&#x209c;&#x2100;-&#x214f;0-9]*" />
<RegExpr attribute="Hexadecimal" context="#stay" String="0[xX][0-9a-fA-F]+" />
<RegExpr attribute="Float" context="#stay" String="[0-9]+(?:(\.[0-9]*)?[eE][+-]?[0-9]+|\.[0-9]*)" />
<RegExpr attribute="Decimal" context="#stay" String="[0-9]+" />
<DetectChar attribute="String" context="string" char="&quot;" />
<StringDetect attribute="Comment" context="#stay" String="/--/" />
<StringDetect attribute="DocComment" context="DocMultiLineComment" String="/-!" />
<StringDetect attribute="DocComment" context="DocMultiLineComment" String="/--" />
<StringDetect attribute="Comment" context="MultiLineComment" String="/-" />
<StringDetect lookAhead="true" context="SingleLineComment" String="--" />
<!-- <StringDetect attribute="Operation" context="#stay" String="..." />
<StringDetect attribute="Operation" context="#stay" String="<;>" />
<StringDetect attribute="Operation" context="#stay" String="|-" />
<StringDetect attribute="Operation" context="#stay" String=":=" />
<StringDetect attribute="Operation" context="#stay" String="!=" />
<StringDetect attribute="Operation" context="#stay" String="#&amp;" />
<StringDetect attribute="Operation" context="#stay" String="-." />
<StringDetect attribute="Operation" context="#stay" String="->" />
<StringDetect attribute="Operation" context="#stay" String=".." />
<StringDetect attribute="Operation" context="#stay" String="::" />
<StringDetect attribute="Operation" context="#stay" String=":>" />
<StringDetect attribute="Operation" context="#stay" String=";;" />
<StringDetect attribute="Operation" context="#stay" String="&lt;-" />
<StringDetect attribute="Operation" context="#stay" String="==" />
<StringDetect attribute="Operation" context="#stay" String="||" />
<StringDetect attribute="Operation" context="#stay" String="&lt;-" />
<StringDetect attribute="Operation" context="#stay" String="=>" />
<StringDetect attribute="Operation" context="#stay" String="&lt;=" />
<StringDetect attribute="Operation" context="#stay" String=">=" />
<StringDetect attribute="Operation" context="#stay" String="/\" />
<StringDetect attribute="Operation" context="#stay" String="\/" />
<StringDetect attribute="Operation" context="#stay" String="⁻¹" />
<AnyChar attribute="Operation" context="#stay"
String="#&amp;*+-/@!`.;&lt;=>_|~∀Πλ↔∧∨≠≤≥¬⬝▸←→∃≈×⌞⌟≡⟨⟩⊢‹›" />
<AnyChar attribute="Constants" context="#stay" String="ℕℤ" /> -->
</context>
<context attribute="Comment" lineEndContext="#pop" name="SingleLineComment">
</context>
<context attribute="Comment" lineEndContext="#stay" name="MultiLineComment">
<StringDetect attribute="Comment" context="#pop" String="-/" />
<StringDetect attribute="Comment" context="#stay" String="/--/" />
<StringDetect attribute="DocComment" context="DocMultiLineComment" String="/-!" />
<StringDetect attribute="DocComment" context="DocMultiLineComment" String="/--" />
<StringDetect attribute="Comment" context="MultiLineComment" String="/-" />
</context>
<context attribute="DocComment" lineEndContext="#stay" name="DocMultiLineComment">
<StringDetect attribute="DocComment" context="#pop" String="-/" />
<StringDetect attribute="Comment" context="#stay" String="/--/" />
<StringDetect attribute="DocComment" context="DocMultiLineComment" String="/-!" />
<StringDetect attribute="DocComment" context="DocMultiLineComment" String="/--" />
<StringDetect attribute="Comment" context="MultiLineComment" String="/-" />
</context>
<context attribute="String" lineEndContext="#stay" name="string">
<DetectChar attribute="String" context="#pop" char="&quot;" />
<RegExpr attribute="StringEscape" context="#stay"
String="\\(?:[\\&quot;ntr']|x[0-9A-Fa-f]{2}|u[0-9A-Fa-f]{4})" />
<DetectChar attribute="ErrorStringEscape" context="#stay" char="\" />
</context>
<context attribute="Importing" lineEndContext="#pop" name="Importing">
</context>
<context attribute="Defining" lineEndContext="#stay" name="defining">
<keyword attribute="DefinitionsAfterName" context="#pop"
String="DefinitionsAfterName" />
<AnyChar attribute="String" context="#pop" String="&quot;:|([{⦃&lt;>"
lookAhead="true" />
</context>
</contexts>
<itemDatas>
<itemData name="Normal Text" defStyleNum="dsNormal" spellChecking="false" />
<itemData name="Types" defStyleNum="dsBuiltIn" spellChecking="false" />
<itemData name="Modifiers" defStyleNum="dsAttribute" spellChecking="false" />
<itemData name="sorry" defStyleNum="dsWarning" spellChecking="false" />
<itemData name="Commands" defStyleNum="dsPreprocessor" spellChecking="false" />
<itemData name="import" defStyleNum="dsKeyword" spellChecking="false" />
<itemData name="ControlFlows" defStyleNum="dsControlFlow" spellChecking="false" />
<itemData name="Definitions" defStyleNum="dsKeyword" spellChecking="false" />
<itemData name="DefinitionsAfterName" defStyleNum="dsKeyword" spellChecking="false" />
<!-- <itemData name="Operation" defStyleNum="dsOperator" spellChecking="false"/> -->
<itemData name="Tactics" defStyleNum="dsKeyword" spellChecking="false" />
<itemData name="Keywords" defStyleNum="dsKeyword" spellChecking="false" />
<itemData name="Constants" defStyleNum="dsConstant" spellChecking="false" />
<itemData name="NameEscape" defStyleNum="dsNormal" spellChecking="false" />
<itemData name="Name" defStyleNum="dsNormal" spellChecking="false" />
<itemData name="Hexadecimal" defStyleNum="dsBaseN" spellChecking="false" />
<itemData name="Float" defStyleNum="dsFloat" spellChecking="false" />
<itemData name="Decimal" defStyleNum="dsDecVal" spellChecking="false" />
<itemData name="Defining" defStyleNum="dsFunction" spellChecking="false" />
<itemData name="Importing" defStyleNum="dsImport" spellChecking="false" />
<itemData name="String" defStyleNum="dsString" spellChecking="false" />
<itemData name="StringEscape" defStyleNum="dsSpecialChar" spellChecking="false" />
<itemData name="ErrorStringEscape" defStyleNum="dsError" spellChecking="false" />
<itemData name="Comment" defStyleNum="dsComment" />
<itemData name="DocComment" defStyleNum="dsDocumentation" />
</itemDatas>
</highlighting>
<general>
<comments>
<comment name="singleLine" start="--" position="afterwhitespace" />
<comment name="multiLine" start="/-" end="-/" />
</comments>
<keywords casesensitive="1" weakDeliminator="#._"
additionalDeliminator="#&amp;*+-/!`;&lt;=>_|~∀Πλ↔∧∨≠≤≥¬·⬝▸←→∃≈×⌞⌟≡⟨⟩⊢‹›⦃⦄" />
<folding indentationsensitive="1" />
</general>
</language>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment