% 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

\lstdefinelanguage{lean} {

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

% keywords
morekeywords=[1]{
import, prelude, tactic_hint, protected, private, definition, renaming,
hiding, exposing, parameter, parameters, begin, begin+, proof, qed, conjecture, constant, constants,
hypothesis, lemma, corollary, variable, variables, premise, premises,
print, theorem, example, abbreviation,
open, as, export, axiom, axioms, inductive, with, structure, record, universe, universes,
alias, help, environment, options, precedence, reserve,
match, infix, infixl, infixr, notation, postfix, prefix,
tactic_infix, tactic_infixl, tactic_infixr, tactic_notation, tactic_postfix, tactic_prefix,
eval, check, coercion, end, reveal,
using, namespace, section, fields, find_decl,
attribute, local, set_option, add_rewrite, extends, include, omit, classes,
instances, coercions, metaclasses, raw, migrate, replacing,
calc, have, obtains, show, by, by+, in, at, let, forall, fun,
exists, if, dif, then, else, assume, assert, take, obtain, from
},

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

% tactics
morekeywords=[3]{
Cond, or_else, then, try, when, assumption, eassumption, rapply,
apply, fapply, eapply, rename, intro, intros, all_goals, fold,
generalize, generalizes, clear, clears, revert, reverts, back, beta, done, exact, rexact,
refine, repeat, whnf, rotate, rotate_left, rotate_right, inversion, cases, rewrite, esimp,
unfold, change, check_expr, contradiction, exfalso, split, existsi, constructor, left, right,
injection, congruence, reflexivity, symmetry, transitivity, state, induction, induction_using
},

% attributes
morekeywords=[4]{
\[persistent\], \[notation\], \[visible\], \[instance\], \[class\], \[parsing-only\],
\[coercion\], \[unfold-f\], \[constructor\], \[reducible\],
\[irreducible\], \[semireducible\], \[quasireducible\], \[wf\],
\[whnf\], \[multiple-instances\], \[none\],
\[decls\], \[declarations\], \[coercions\], \[classes\],
\[symm\], \[subst\], \[refl\], \[trans\], \[recursor\],
\[notations\], \[abbreviations\], \[begin-end-hints\], \[tactic-hints\],
\[reduce-hints\], \[unfold-hints\], \[aliases\], \[eqv\], \[localrefinfo\]
},

% 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{\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

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

{≤}{{\ensuremath{\leq}}}1
{≥}{{\ensuremath{\geq}}}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{\cdot}}}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{\vdash}}}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{\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{\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{_1}}}1
{₂}{{\ensuremath{_2}}}1
{₃}{{\ensuremath{_3}}}1
{₄}{{\ensuremath{_4}}}1
{₅}{{\ensuremath{_5}}}1
{₆}{{\ensuremath{_6}}}1
{₇}{{\ensuremath{_7}}}1
{₈}{{\ensuremath{_8}}}1
{₉}{{\ensuremath{_9}}}1
{₀}{{\ensuremath{_0}}}1

{¹}{{\ensuremath{^1}}}1

{ₙ}{{\ensuremath{_n}}}1
{ₘ}{{\ensuremath{_m}}}1
{↑}{{\ensuremath{\uparrow}}}1
{↓}{{\ensuremath{\downarrow}}}1

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

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

{:=}{{\color{symbolcolor}:=}}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][\itshape \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 tactics keywords
keywordstyle=[3]{\ttfamily\color{tacticcolor}},

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

% Style for strings
stringstyle=\ttfamily,

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

}