diff --git a/extras/latex/lstlean.md b/extras/latex/lstlean.md
new file mode 100644
index 0000000000..fb8dc4340e
--- /dev/null
+++ b/extras/latex/lstlean.md
@@ -0,0 +1,49 @@
+lstlean.tex
+===========
+
+The file `lstlean.tex` contains /Lean/ style definitions for the
+`listings` package, which can be used to typeset Lean code in a
+Latex document. For more information, see the documentation for the
+`listings` package and the sample document `sample.tex`.
+
+You need the following packages installed:
+
+- `listings`
+- `inputenc`
+- `color`
+
+Because `listings` does not work well with unicode, the style
+replaces all unicode characters with Latex equivalents. Some of the
+replacment symbols require the `amssymb` package.
+
+To use the style, all you need to do is include `lstlean.tex` in
+the same directory as your Latex source, and include the following
+preamble in your document:
+```
+\documentclass{article}
+
+\usepackage[utf8x]{inputenc}
+\usepackage{amssymb}
+
+\usepackage{color}
+\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
+\definecolor{tacticcolor}{rgb}{0.1, 0.2, 0.6}    % blue
+\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
+\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
+\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
+\definecolor{attributecolor}{rgb}{0.7, 0.1, 0.1} % red
+
+\usepackage{listings}
+\def\lstlanguagefiles{lstlean.tex}
+\lstset{language=lean}
+```
+
+The `inputenc` package is needed to handle unicode input. Of
+course, you can set the colors any way you want. In your document,
+you can then in-line code with the `\lstinline{...}`, and add a code
+block with the `\begin{lstlisting} ... \end{lstlisting}`
+environment.
+
+Note that if you use a unicode symbol that is not currently handled in
+`lstlean.tex`, you can simply add it to the list there, together
+with the Latex equivalent you would like to use.
diff --git a/extras/latex/lstlean.tex b/extras/latex/lstlean.tex
new file mode 100644
index 0000000000..5b14ee8c0e
--- /dev/null
+++ b/extras/latex/lstlean.tex
@@ -0,0 +1,272 @@
+% 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 },
+
+}
+
diff --git a/extras/latex/sample.tex b/extras/latex/sample.tex
new file mode 100644
index 0000000000..9d624b4567
--- /dev/null
+++ b/extras/latex/sample.tex
@@ -0,0 +1,72 @@
+\documentclass{article}
+
+\usepackage[utf8x]{inputenc}
+\usepackage{amssymb}
+
+\usepackage{color}
+\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
+\definecolor{tacticcolor}{rgb}{0.1, 0.2, 0.6}    % blue
+\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
+\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
+\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
+\definecolor{attributecolor}{rgb}{0.7, 0.1, 0.1} % red
+
+\usepackage{listings}
+\def\lstlanguagefiles{lstlean.tex}
+\lstset{language=lean}
+
+\title{The Lean listing style}
+\author{Jeremy Avigad}
+
+\begin{document}
+
+\maketitle 
+
+This is an example of how to use \verb=lstlean.tex= to typeset your Lean code. Here is some code: \lstinline{theorem foo (x y : ℕ), x + y = y + x}.  Here are the translations of some unicode symbols:
+\begin{lstlisting}
+Some symbols: ℕ ℤ ∩ ⊂ ∀ ∃ Π α β γ ∈ ⦃ ⦄
+\end{lstlisting}
+Here is a block of code:
+\begin{lstlisting}
+/-
+Basic properties of lists.
+-/
+import logic tools.helper_tactics data.nat.basic algebra.function
+open eq.ops helper_tactics nat prod function option
+
+inductive list (T : Type) : Type :=
+| nil {} : list T
+| cons   : T → list T → list T
+
+namespace list
+notation h :: t  := cons h t
+notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
+
+variable {T : Type}
+
+/- append -/
+
+definition append : list T → list T → list T
+| []       l := l
+| (h :: s) t := h :: (append s t)
+
+notation l₁ ++ l₂ := append l₁ l₂
+
+theorem append_nil_left (t : list T) : [] ++ t = t
+
+theorem append_cons (x : T) (s t : list T) : (x::s) ++ t = x::(s ++ t)
+
+theorem append_nil_right : ∀ (t : list T), t ++ [] = t
+| []       := rfl
+| (a :: l) := calc
+  (a :: l) ++ [] = a :: (l ++ []) : rfl
+             ... = a :: l         : append_nil_right l
+
+theorem append.assoc : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u)
+| []       t u := rfl
+| (a :: l) t u :=
+  show a :: (l ++ t ++ u) = (a :: l) ++ (t ++ u),
+  by rewrite (append.assoc l t u)
+\end{lstlisting}
+
+\end{document}