class Rouge::Lexers::Lean

def self.keywords
  @keywords ||= Set.new %w(
    abbreviation
    add_rewrite
    alias
    assume
    axiom
    begin
    by
    calc
    calc_refl
    calc_subst
    calc_trans
    #check
    coercion
    conjecture
    constant
    constants
    context
    corollary
    def
    definition
    end
    #eval
    example
    export
    expose
    exposing
    exit
    extends
    from
    fun
    have
    help
    hiding
    hott
    hypothesis
    import
    include
    including
    inductive
    infix
    infixl
    infixr
    inline
    instance
    irreducible
    lemma
    match
    namespace
    notation
    opaque
    opaque_hint
    open
    options
    parameter
    parameters
    postfix
    precedence
    prefix
    #print
    private
    protected
    #reduce
    reducible
    renaming
    repeat
    section
    set_option
    show
    tactic_hint
    theorem
    universe
    universes
    using
    variable
    variables
    with
  )
end

def self.operators
  @operators ||= %w(
    != # & && \* \+ - / @ ! ` -\. ->
    \. \.\. \.\.\. :: :> ; ;; <
    <- = == > _ \| \|\| ~ => <= >=
    /\ \/ ∀ Π λ ↔ ∧ ∨ ≠ ≤ ≥ ⊎
    ¬ ⁻¹ ⬝ ▸ → ∃ ℕ ℤ ≈ × ⌞ ⌟ ≡ ⟨ ⟩
  )
end

def self.types
  @types ||= %w(
    Sort
    Prop
    Type
  )
end