class Rouge::Lexers::Lean
Public Class Methods
keywords()
click to toggle source
# File lib/rouge/lexers/lean.rb, line 12 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()
click to toggle source
# File lib/rouge/lexers/lean.rb, line 101 def self.operators @operators ||= %w( != # & && \* \+ - / @ ! ` -\. -> \. \.\. \.\.\. :: :> ; ;; < <- = == > _ \| \|\| ~ => <= >= /\ \/ ∀ Π λ ↔ ∧ ∨ ≠ ≤ ≥ ⊎ ¬ ⁻¹ ⬝ ▸ → ∃ ℕ ℤ ≈ × ⌞ ⌟ ≡ ⟨ ⟩ ) end
types()
click to toggle source
# File lib/rouge/lexers/lean.rb, line 93 def self.types @types ||= %w( Sort Prop Type ) end