feat(extras/latex/*): add listings style definition and instructions
This commit is contained in:
Jeremy Avigad
parent
566acf4b31
commit
18742e8ab8
3 changed files with 393 additions and 0 deletions
49
extras/latex/lstlean.md
Normal file
49
extras/latex/lstlean.md
Normal file
|
|
@ -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.
|
||||
272
extras/latex/lstlean.tex
Normal file
272
extras/latex/lstlean.tex
Normal file
|
|
@ -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 },
|
||||
|
||||
}
|
||||
|
||||
72
extras/latex/sample.tex
Normal file
72
extras/latex/sample.tex
Normal file
|
|
@ -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}
|
||||
Loading…
Reference in a new issue