<?xml version="1.0" encoding="utf-8"?>

<!-- 
Lean syntax highlighting
Written by Ezra Altahan
Created 12/08/2016 | Updated 16/10/2016
Version 1.0

hello@exr.be
https://github.com/ei
-->

<SyntaxDefinition name="Lean" extensions=".lean;.hlean">
    
    <Environment> 
        <Default color="Black" bgcolor="#FFFFFF"/>
        <Selection color="Black" bgcolor="#C3C3FF"/>
        <LineNumbers color="Gray" bgcolor="#FFFFFF"/>
        <CaretMarker color="#F0F0F1"/>
        <VRuler color="#E0E0E5"/>
        
        <FoldLine color="#A0A0A0" bgcolor="#FFFFFF"/>
        <FoldMarker color="Black" bgcolor="#FFFFFF"/>
        <SelectedFoldLine color="Black" bgcolor="#FFFFFF"/>
        
        <EOLMarkers color="#CACAD2"/>
        <SpaceMarkers color="#B6B6C0"/>
        <TabMarkers color="#B6B6C0"/>
        <InvalidLines color="#B6B6C0"/>
    </Environment>
    
    <Properties>
        <Property name="LineComment" value="--"/>
        <Property name="BlockCommentBegin" value="/-"/>
        <Property name="BlockCommentEnd" value="-/"/>
    </Properties>
    
<Digits name="Digits" color="#DF7000"/>
    
    <RuleSets>
        <RuleSet ignorecase="false">
        
            <Delimiters>&amp;&lt;&gt;~!%^*()-+=|\/{}.:;"' , ?</Delimiters>
        
            <Span name="LineComment" stopateol="true" color="Green" bold="false" italic="false">
                <Begin>--</Begin>
            </Span>
            
            <Span name="BlockComment" stopateol="false" color="Green" bold="false" italic="false">
                <Begin>/-</Begin>
                <End>-/</End>
            </Span>
            
            <Span name="String" stopateol="false" color="#808080" bold="false" italic="false" escapecharacter="\">
                <Begin>"</Begin>
                <End>"</End>
            </Span>
            
            <MarkFollowing color="#C82829" bold="false" italic="false">axiom</MarkFollowing>
            <MarkFollowing color="#C82829" bold="false" italic="false">definition</MarkFollowing>
            <MarkFollowing color="#C82829" bold="false" italic="false">inductive</MarkFollowing>
            <MarkFollowing color="#C82829" bold="false" italic="false">structure</MarkFollowing>
            <MarkFollowing color="#C82829" bold="false" italic="false">theorem</MarkFollowing>
            
            <KeyWords name="Keywords1" color="Blue" bold="false">
                <Key word="as"/>
                <Key word="assume"/>
                <Key word="attribute"/>
                <Key word="axiom"/>
                <Key word="axioms"/>
                <Key word="begin"/>
                <Key word="by"/>
                <Key word="calc"/>
                <Key word="check"/>
                <Key word="coercions"/>
                <Key word="constant"/>
                <Key word="constants"/>
                <Key word="definition"/>
                <Key word="else"/>
                <Key word="end"/>
                <Key word="eval"/>
                <Key word="example"/>
                <Key word="exists"/>
                <Key word="exit"/>
                <Key word="export"/>
                <Key word="forall"/>
                <Key word="from"/>
                <Key word="fun"/>
                <Key word="have"/>
                <Key word="if"/>
                <Key word="import"/>
                <Key word="inductive"/>
                <Key word="infix"/>
                <Key word="infixl"/>
                <Key word="lemma"/>
                <Key word="namespace"/>
                <Key word="noncomputable"/>
                <Key word="notation"/>
                <Key word="open"/>
                <Key word="parameter"/>
                <Key word="precedence"/>
                <Key word="prelude"/>
                <Key word="print"/>
                <Key word="raw"/>
                <Key word="reserve"/>
                <Key word="section"/>
                <Key word="set_option"/>
                <Key word="show"/>
                <Key word="structure"/>
                <Key word="take"/>
                <Key word="then"/>
                <Key word="theorem"/>
                <Key word="universe"/>
                <Key word="universes"/>
                <Key word="variable"/>
                <Key word="variables"/>
                <Key word="with"/>
            </KeyWords>
            
            <KeyWords name="Keywords2" color="DarkViolet" bold="false">
                <Key word="Prop"/>
                <Key word="Type"/>
                <Key word="Type₁"/>
                <Key word="Type₂"/>
                <Key word="Type₃"/>
                <Key word="[class]"/>
                <Key word="[coercion]"/>
                <Key word="[constructor]"/>
                <Key word="[instance]"/>
                <Key word="[irreducible]"/>
                <Key word="[recursor]"/>
                <Key word="[reducible]"/>
                <Key word="[refl]"/>
                <Key word="[semireducible]"/>
                <Key word="[simp]"/>
                <Key word="[symm]"/>
                <Key word="[trans]"/>
            </KeyWords>         
        </RuleSet>
    </RuleSets>
</SyntaxDefinition>
