Class: Rouge::Lexers::Lean

Inherits:
RegexLexer show all
Defined in:
lib/rouge/lexers/lean.rb

Constant Summary

Constants inherited from RegexLexer

RegexLexer::MAX_NULL_SCANS

Constants included from Token::Tokens

Token::Tokens::Num, Token::Tokens::Str

Instance Attribute Summary

Attributes inherited from Rouge::Lexer

#options

Class Method Summary collapse

Methods inherited from RegexLexer

append, #delegate, get_state, #get_state, #goto, #group, #groups, #in_state?, #pop!, prepend, #push, #recurse, replace_state, #reset!, #reset_stack, #stack, start, start_procs, #state, state, #state?, state_definitions, states, #step, #stream_tokens, #token

Methods inherited from Rouge::Lexer

aliases, all, #as_bool, #as_lexer, #as_list, #as_string, #as_token, assert_utf8!, #bool_option, #continue_lex, continue_lex, debug_enabled?, demo, demo_file, desc, detect?, detectable?, disable_debug!, enable_debug!, filenames, find, find_fancy, guess, guess_by_filename, guess_by_mimetype, guess_by_source, guesses, #hash_option, #initialize, lex, #lex, #lexer_option, #list_option, lookup_fancy, mimetypes, option, option_docs, #reset!, #stream_tokens, #string_option, tag, #tag, title, #token_option, #with

Methods included from Token::Tokens

token

Constructor Details

This class inherits a constructor from Rouge::Lexer

Class Method Details

.keywords ⇒ Object 



14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
 
# File 'lib/rouge/lexers/lean.rb', line 14

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

.operators ⇒ Object 



103
104
105
106
107
108
109
110
111
 
# File 'lib/rouge/lexers/lean.rb', line 103

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

.types ⇒ Object 



95
96
97
98
99
100
101
 
# File 'lib/rouge/lexers/lean.rb', line 95

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