agda/test/LaTeXAndHTML/user-manual/beamer-pdflatex.tex

\documentclass{beamer}

% Use the input encoding UTF-8 and the font encoding T1.
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}

% Support for Agda code.
\usepackage{agda}

% Decrease the indentation of code.
\setlength{\mathindent}{1em}

% Customised setup for certain characters.
\usepackage{newunicodechar}
\newunicodechar{∀}{\ensuremath{\mathnormal{\forall}}}
\newunicodechar{→}{\ensuremath{\mathnormal{\to}}}
\newunicodechar{₁}{\ensuremath{{}_1}}

% Support for Greek letters.
\usepackage{alphabeta}

% Disable ligatures that start with '-'. Note that this affects the
% entire document!
\usepackage{microtype}
\DisableLigatures[-]{encoding=T1}

\begin{document}

\begin{frame}
  Some code:
  \begin{code}%
%
\>[2]\AgdaSymbol{\{-\#}\AgdaSpace{}%
\AgdaKeyword{OPTIONS}\AgdaSpace{}%
\AgdaPragma{--without-K}\AgdaSpace{}%
\AgdaPragma{--count-clusters}\AgdaSpace{}%
\AgdaSymbol{\#-\}}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
%
\>[2]\AgdaKeyword{open}\AgdaSpace{}%
\AgdaKeyword{import}\AgdaSpace{}%
\AgdaModule{Agda.Builtin.String}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
%
\>[2]\AgdaComment{--\ A\ comment\ with\ some\ TeX\ ligatures:}\<%
\\
%
\>[2]\AgdaComment{--\ --,\ ---,\ ?`,\ !`,\ `,\ ``,\ ',\ '',\ <<,\ >>.}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
%
\>[2]\AgdaFunction{Θ₁}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\\
%
\>[2]\AgdaFunction{Θ₁}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{λ}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{A}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
%
\>[2]\AgdaFunction{a-name-with--hyphens}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{∀}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{A}\<%
\\
%
\>[2]\AgdaFunction{a-name-with--hyphens}\AgdaSpace{}%
\AgdaBound{ff--fl}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaBound{ff--fl}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
%
\>[2]\AgdaFunction{ffi}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPostulate{String}\<%
\\
%
\>[2]\AgdaFunction{ffi}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaString{"--"}\<%
\end{code}
  Note that the code is indented.
\end{frame}

\end{document}