Foo.lagda.tex

%% This file was automatically generated by agda2lagda 0.2023.6.9.

\heading{Sample non-literate Agda program}

A remark to test bulleted lists:

\begin{itemize}

\item
This file serves as example for agda2lagda.

\item
The content may be non-sensical.

\end{itemize}

Indeed!

\begin{code}
module Foo where
\end{code}

Some data type.

\begin{code}
data D : Set where
  c : D
\end{code}

A function.

\begin{code}
foo : D → D
foo c = c   -- basically, the identity
\end{code}

%% This part is commented out.
%% {-
%% bar : D → Set
%% bar x = D
%% -- -}
%% --

\subheading{A subheading}

\begin{code}
module Submodule where

  postulate
    zeta : D
\end{code}

That's it.
Bye.