agda/test/LaTeXAndHTML/succeed/Inline.tex

\documentclass{article}

\usepackage{agda}

\begin{document}

Assume that we are given a type
%
\begin{code}[inline=False,hide=true]%
%
\>[2]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{(}\<%
\end{code}
\begin{code}[hide,inline,hide=false]%
\>[2][@{}l@{\AgdaIndent{1}}]%
\>[4]\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\begin{code}[hide=false,hide=True]%
%
\>[4]\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\<%
\end{code}
%
,
and that a function
%
\begin{code}[inline*]%
%
\>[4]\AgdaBound{F}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\begin{code}[hide]%
%
\>[4]\AgdaSymbol{)}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\end{code}
%
is also given.

\end{document}