% Listing style definition for the Lean Theorem Prover.
% Defined by Jeremy Avigad, 2015, by modifying Assia Mahboubi's SSR style.
% Unicode replacements taken from Olivier Verdier's unixode.sty
% Extensions by Jasmin Blanchette.

\lstdefinelanguage{leanx} {

% Anything betweeen $ becomes LaTeX math mode
mathescape=true,
% Comments may or not include Latex commands
texcl=false,

alsoletter={\#.0123456789'},

procnamekeys={theorem,lemma,def,inductive,structure,class,instance,axiom,opaque},

% keywords, list taken from lean-syntax.el
morekeywords=[1]{
import, prelude, protected, private, definition, renaming,
hiding, exposing, parameter, parameters, begin, conjecture,
lemma, corollary, variable, variables, premise, premises, theory,
\#find, \#print, theorem, proposition, example, abstract,
open, export, override, axiom, axioms, inductive, without,
structure, record, universe, universes,
alias, help, precedence, reserve, declare_trace, add_key_equivalence,
infix, infixl, infixr, notation, postfix, prefix, instance,
\#eval, vm_eval, \#check, \#reduce, coercion, this, suppose,
using, using_well_founded, namespace, section, fields,
attribute, local, set_option, extends, include, omit, classes, class,
instances, coercions, attributes, raw, replacing,
calc, have, show, suffices, by, Pi, fun,
dif, fix, assume, take, obtain, from, aliases, register_simp_ext,
mutual, partial, def, elab, run_cmd, match, with, end, do, let, in, where,
fun, opaque,
ac_rfl, apply, assumption, clear, exact, induction, cases, intro, rename,
rw, rfl, simp, aesop, linarith,
for, if, then, else, mut, return, continue, try, catch,
macro, repeat', any_goals, solve, all_goals, first, intro_and_even, trace_goals,
destruct_and, prove_direct, hypothesis, done, skip, at, generalizing, noncomputable,
library_search, decide, norm_cast, ring, abel
},

% Sorts
morekeywords=[2]{Type, Prop, Type*, Sort},

% Sorry
morekeywords=[3]{sorry},

% Numbers
morekeywords=[4]{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11, 12, 13, 14, 15, 16, 17, 18,
19, 20, 21, 22, 23, 24, 30, 31, 32, 33, 40, 42, 666, 999},

% tactics, list taken from lean-syntax.el
% morekeywords=[3]{
% Cond, or_else, then, try, when, assumption, eassumption, rapply,
% apply, fapply, eapply, rename, intro, intros, all_goals, fold, focus, focus_at,
% generalize, generalizes, clear, clears, revert, reverts, back, beta, done, exact, rexact,
% refine, repeat, whnf, rotate, rotate_left, rotate_right, inversion, cases, rewrite,
% xrewrite, krewrite, blast, simp, esimp, unfold, change, check_expr, contradiction,
% exfalso, split, existsi, constructor, fconstructor, left, right, injection, congruence, reflexivity,
% symmetry, transitivity, state, induction, induction_using, fail, append,
% substvars, now, with_options, with_attributes, with_attrs, note
% },

% Modifiers, inner keyowrds
morekeywords=[5]{},

% modifiers, taken from lean-syntax.el
% note: 'otherkeywords' is needed because these use a different symbol.
% this command doesn't allow us to specify a number -- they are put with [1]
otherkeywords={
@[persistent], @[notation], @[visible], @[instance], @[trans_instance],
@[class], @[parsing-only], @[coercion], @[unfold_full], @[constructor],
@[reducible], @[irreducible], @[semireducible], @[quasireducible], @[wf],
@[whnf], @[multiple_instances], @[none], @[decl], @[declaration],
@[relation], @[symm], @[subst], @[refl], @[trans], @[simp], @[congr], @[unify],
@[backward], @[forward], @[no_pattern], @[begin_end], @[tactic], @[abbreviation],
@[reducible], @[unfold], @[alias], @[eqv], @[intro], @[intro!], @[elim], @[grinder],
@[localrefinfo], @[recursor]
},

% Various symbols
literate=
{α}{{\ensuremath{\mathrm{\alpha}}}}1
{β}{{\ensuremath{\mathrm{\beta}}}}1
{γ}{{\ensuremath{\mathrm{\gamma}}}}1
{δ}{{\ensuremath{\mathrm{\delta}}}}1
{ε}{{\ensuremath{\mathrm{\varepsilon}}}}1
{ζ}{{\ensuremath{\mathrm{\zeta}}}}1
{η}{{\ensuremath{\mathrm{\eta}}}}1
{θ}{{\ensuremath{\mathrm{\theta}}}}1
{ι}{{\ensuremath{\mathrm{\iota}}}}1
{κ}{{\ensuremath{\mathrm{\kappa}}}}1
{μ}{{\ensuremath{\mathrm{\mu}}}}1
{ν}{{\ensuremath{\mathrm{\nu}}}}1
{ξ}{{\ensuremath{\mathrm{\xi}}}}1
{π}{{\ensuremath{\mathrm{\mathnormal{\pi}}}}}1
{ρ}{{\ensuremath{\mathrm{\rho}}}}1
{σ}{{\ensuremath{\mathrm{\sigma}}}}1
{τ}{{\ensuremath{\mathrm{\tau}}}}1
{υ}{{\ensuremath{\mathrm{\upsilon}}}}1
{φ}{{\ensuremath{\mathrm{\varphi}}}}1
{χ}{{\ensuremath{\mathrm{\chi}}}}1
{ψ}{{\ensuremath{\mathrm{\psi}}}}1
{ω}{{\ensuremath{\mathrm{\omega}}}}1

{Γ}{{\ensuremath{\mathrm{\Gamma}}}}1
{Δ}{{\ensuremath{\mathrm{\Delta}}}}1
{Θ}{{\ensuremath{\mathrm{\Theta}}}}1
{Λ}{{\ensuremath{\mathrm{\Lambda}}}}1
{Σ}{{\ensuremath{\mathrm{\Sigma}}}}1
{Φ}{{\ensuremath{\mathrm{\Phi}}}}1
{Ξ}{{\ensuremath{\mathrm{\Xi}}}}1
{Ψ}{{\ensuremath{\mathrm{\Psi}}}}1
{Ω}{{\ensuremath{\mathrm{\Omega}}}}1

{ℵ}{{\ensuremath{\aleph}}}1

{`}{{\reflectbox{\texttt{'}}}}1

%{<}{{\ensuremath{<}}}1
{≤}{{\ensuremath{\leq}}}1
%{>}{{\ensuremath{>}}}1
{≥}{{\ensuremath{\geq}}}1
{≠}{{\ensuremath{\neq}}}1
{≈}{{\ensuremath{\approx}}}1
{≡}{{\ensuremath{\equiv}}}1
{≃}{{\ensuremath{\simeq}}}1

{∂}{{\ensuremath{\partial}}}1
{∆}{{\ensuremath{\triangle}}}1 % or \laplace?

{∫}{{\ensuremath{\int}}}1
{∑}{{\ensuremath{\mathrm{\Sigma}}}}1
{Π}{{\ensuremath{\mathrm{\Pi}}}}1

{⊥}{{\ensuremath{\perp}}}1
{∞}{{\ensuremath{\infty}}}1
{∂}{{\ensuremath{\partial}}}1

{∓}{{\ensuremath{\mp}}}1
{±}{{\ensuremath{\pm}}}1
{×}{{\ensuremath{\times}}}1

{⊕}{{\ensuremath{\oplus}}}1
{⊗}{{\ensuremath{\otimes}}}1
{⊞}{{\ensuremath{\boxplus}}}1

{∇}{{\ensuremath{\nabla}}}1
{√}{{\ensuremath{\sqrt}}}1

{⬝}{{\ensuremath{\cdot}}}1
{•}{{\ensuremath{\bullet}}}1
{∘}{{\ensuremath{\circ}}}1

%{⁻}{{\ensuremath{^{\textup{\kern1pt\rule{2pt}{0.3pt}\kern-1pt}}}}}1
{⁻}{{\ensuremath{^{-}}}}1
{▸}{{\ensuremath{\blacktriangleright}}}1

{∧}{{\ensuremath{\wedge}}}1
{∨}{{\ensuremath{\vee}}}1
{¬}{{\ensuremath{\neg}}}1

%{⟨}{{\ensuremath{\left\langle}}}1
%{⟩}{{\ensuremath{\right\rangle}}}1
{⟨}{{\ensuremath{\langle}}}1
{⟩}{{\ensuremath{\rangle}}}1

{↦}{{\ensuremath{\mapsto}}}1
{→}{{\ensuremath{\rightarrow}}}1
{↔}{{\ensuremath{\leftrightarrow}}}1
{⇒}{{\ensuremath{\Rightarrow}}}1
{⟹}{{\ensuremath{\Longrightarrow}}}1
{⇐}{{\ensuremath{\Leftarrow}}}1
{←}{{\ensuremath{\leftarrow}}}1
{⟸}{{\ensuremath{\Longleftarrow}}}1

{∩}{{\ensuremath{\cap}}}1
{∪}{{\ensuremath{\cup}}}1
{⊂}{{\ensuremath{\subseteq}}}1
{⊆}{{\ensuremath{\subseteq}}}1
{⊄}{{\ensuremath{\nsubseteq}}}1
{⊈}{{\ensuremath{\nsubseteq}}}1
{⊃}{{\ensuremath{\supseteq}}}1
{⊇}{{\ensuremath{\supseteq}}}1
{⊅}{{\ensuremath{\nsupseteq}}}1
{⊉}{{\ensuremath{\nsupseteq}}}1
{∈}{{\ensuremath{\in}}}1
{∉}{{\ensuremath{\notin}}}1
{∋}{{\ensuremath{\ni}}}1
{∌}{{\ensuremath{\notni}}}1
{∅}{{\ensuremath{\emptyset}}}1
{◯}{{\ensuremath{\fullmoon}}}1
{⨅}{{\ensuremath{\bigsqcap}}}1

{∖}{{\ensuremath{\setminus}}}1
{†}{{\ensuremath{\dag}}}1

{ℕ}{{\ensuremath{\mathbb{N}}}}1
{ℤ}{{\ensuremath{\mathbb{Z}}}}1
{ℝ}{{\ensuremath{\mathbb{R}}}}1
{ℚ}{{\ensuremath{\mathbb{Q}}}}1
{ℂ}{{\ensuremath{\mathbb{C}}}}1
{⌞}{{\ensuremath{\llcorner}}}1
{⌟}{{\ensuremath{\lrcorner}}}1
{⦃}{{\ensuremath{\{\!|}}}1
{⦄}{{\ensuremath{|\!\}}}}1
{⟦}{{\ensuremath{\llbracket}}}1
{⟧}{{\ensuremath{\rrbracket}}}1

{…}{{\ensuremath{\ldots}}}1
{⋯}{{\ensuremath{\cdots}}}1
{⋮}{{\ensuremath{\vdots}}}1

{–}{\hbox{\textrm{--}}}1
{—}{\hbox{\textrm{---}}}1

{₁}{{\ensuremath{_\texttt{1}}}}1
{₂}{{\ensuremath{_\texttt{2}}}}1
{₃}{{\ensuremath{_\texttt{3}}}}1
{₄}{{\ensuremath{_\texttt{4}}}}1
{₅}{{\ensuremath{_\texttt{5}}}}1
{₆}{{\ensuremath{_\texttt{6}}}}1
{₇}{{\ensuremath{_\texttt{7}}}}1
{₈}{{\ensuremath{_\texttt{8}}}}1
{₉}{{\ensuremath{_\texttt{9}}}}1
{₀}{{\ensuremath{_\texttt{0}}}}1

{¹}{{\ensuremath{^1}}}1
{²}{{\ensuremath{^2}}}1

{ₖ}{{\ensuremath{_\ttvar{k}}}}1
{ₗ}{{\ensuremath{_\ttvar{l}}}}1
{ₘ}{{\ensuremath{_\ttvar{m}}}}1
{ₙ}{{\ensuremath{_\ttvar{n}}}}1
{↑}{{\ensuremath{\uparrow}}}1
{↓}{{\ensuremath{\downarrow}}}1
{⇃}{{\ensuremath{\downharpoonleft}}}1

{▸}{{\ensuremath{\triangleright}}}1

{Σ}{{\ensuremath{\mathrm{\Sigma}}}}1
{Π}{{\ensuremath{\mathrm{\Pi}}}}1
{∀}{{\ensuremath{\forall}}}1
{∃}{{\ensuremath{\exists}}}1
{λ}{{\ensuremath{\mathrm{\lambda}}}}1

{⊢}{{\ensuremath{\color{symbolcolor}\,{\pmb{\vdash}}\,}}}1

{⋂}{{\ensuremath{\bigcap}}}1

{⎧}{}1
{⎨}{}1
{⎧}{}1
{⎨}{}1
{⎩}{}1

{ö}{\"}1
{©}{\copyright{}}1
{↝}{{\ensuremath{\leadsto}}}1,

%{=}{{\color{symbolcolor}=}}1
%{<}{{\color{symbolcolor}<}}1
%{+}{{\color{symbolcolor}+}}1
%{*}{{\color{symbolcolor}*}}1,

% Comments
%comment=[s][\itshape \color{commentcolor}]{/-}{-/},
morecomment=[s][\color{commentcolor}]{/-}{-/},
morecomment=[l][\color{commentcolor}]{--},

% Spaces are not displayed as a special character
showstringspaces=false,

% keep spaces
keepspaces=true,

% String delimiters
morestring=[b]",
morestring=[d],

% Size of tabulations
tabsize=3,

% Enables ASCII chars 128 to 255
extendedchars=false,

% Case sensitivity
sensitive=true,

% Automatic breaking of long lines
breaklines=true,

% Default style fors listingsred
basicstyle=\ttfamily,

% Position of captions is bottom
captionpos=b,

% Full flexible columns
columns=[l]fullflexible,


% Style for (listings') identifiers
identifierstyle={\ttfamily\color{black}},
% Note : highlighting of Coq identifiers is done through a new
% delimiter definition through an lstset at the begining of the
% document. Don't know how to do better.

% Style for declaration keywords
keywordstyle=[1]{\ttfamily\color{keywordcolor}},

% Style for sorts
keywordstyle=[2]{\ttfamily\color{sortcolor}},

% Style for sorry
keywordstyle=[3]{\ttfamily\color{sorrycolor}},

% Style for numbers
keywordstyle=[4]{\ttfamily\color{numeralcolor}},

% Style for modifiers and inner keywords
keywordstyle=[5]{\ttfamily\color{modifiercolor}},

% Style for attributes
% keywordstyle=[4]{\ttfamily\color{attributecolor}},

% Style for strings
stringstyle={\ttfamily\color{stringcolor}},

% Style for comments
% commentstyle={\ttfamily\footnotesize },

% Style for procedures
procnamestyle={\ttfamily\color{procnamecolor}},
}
