71 lines
1.9 KiB
TeX
71 lines
1.9 KiB
TeX
\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
|
||
|
||
\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}
|