test.tex

test.tex

\documentclass{article}
\usepackage{unixode}    % Need to download from https://raw.githubusercontent.com/leanprover/tutorial/master/unixode.sty
\usepackage{minted}     % Need to download from https://raw.githubusercontent.com/leanprover/tutorial/master/minted.sty
% Specify local pygments directory. Do the following in your working directory (where test.tex is located)
% hg clone https://bitbucket.org/leanprover/pygments-main && cd pygments-main && python setup.py build & cd ..
\renewcommand{\MintedPygmentize}{./pygments-main/pygmentize}
\setminted{encoding=utf-8}
\usepackage{fontspec}
\setmainfont{FreeSerif}
\setmonofont{FreeMono}
\usepackage{fullpage}
\usepackage{listings}
\begin{document}
\title{Syntax Highlighter Test}
\maketitle

\begin{minted}[mathescape, linenos, numbersep=5pt, frame=lines, framesep=2mm]{Lean}

definition test1 := Σ n, n = 0
definition test2 := bool ≃ bool
definition test3 := Π P, P → ∥ P ∥

\end{minted}

\end{document}