agda/test/LaTeXAndHTML/succeed/Inline.lagda.tex

\documentclass{article}

\usepackage{agda}

\begin{document}

Assume that we are given a type
%
\begin{code}[inline=False,hide=true]
  module _ (
\end{code}
\begin{code}[hide,inline,hide=false]
    A : Set
\end{code}
\begin{code}[hide=false,hide=True]
    ) (
\end{code}
%
,
and that a function
%
\begin{code}[inline*]
    F : Set → Set → Set → Set
\end{code}
\begin{code}[hide]
    ) where
\end{code}
%
is also given.

\end{document}