source-expected.tex

Using \href{https://github.com/idris-community/katla}{katla}'s pandoc
backend we can produce PDF documents containing semantically highlighted
Idris2 code.

The file you are currently reading is the rendered version of a literate
markdown/idris2 file. It is called \texttt{Source.md} and contains
fenced \texttt{idr} blocks.

\hypertarget{basic-usage}{%
\section{Basic Usage}\label{basic-usage}}

We can hide uninteresting code blocks by adding the \texttt{hide}
attribute. We hide an import of \texttt{Data.Vect} here. We won't see
anything in the output PDF.

We can use all Idris 2 features. Here's an example code block:

\KatlaSnippet{}

And here's a code block in a \LaTeX{} figure environment:

\newcommand\myfig[2]{
    \begin{figure}[h]
    \centering
    #2
    \caption{#1}
    \end{figure}
}

\myfig{Definition of $y$}{

\KatlaSnippet{}

}

We can use namespaces by adding the \texttt{namespace} attribute, such
as to provide alternate definitions for functions. Consider this
function signature:

\KatlaSnippet{}

Here's one implementation for \KatlaSnippet{}:

\KatlaSnippet{}

By repeating the signature in a different namespace, in a hidden code
block, I can give an alternate definition:

\KatlaSnippet{}

\hypertarget{inline-code}{%
\section{Inline Code}\label{inline-code}}

As well as block code, we can have inline code, like
\KatlaSnippet{}. Here's another: \KatlaSnippet{}. We can
also call the function we previously defined: \KatlaSnippet{}.

By default, a code block is interpreted as top-level Idris 2
declarations, while inline code is interpreted as an expression. But we
can switch it up if we wish.

By using the \texttt{decls} class, we can write an inline declaration:
\KatlaSnippet{}.

By using the \texttt{expr} class, we can write a block expression:

\KatlaSnippet{}

\hypertarget{types}{%
\section{Types}\label{types}}

Sometimes, Idris 2 cannot infer the type of an expression. Is
\KatlaSnippet{} a \KatlaSnippet{}, or a
\KatlaSnippet{}? We can use the \texttt{type} attribute to tell
Idris 2 which one it should be.

\hypertarget{multiple-files}{%
\section{Multiple Files}\label{multiple-files}}

If you need an import to \emph{not} be available, namespaces are not
enough. We can use the \texttt{file} attribute to put snippets in
separate files. For example, the signature of \KatlaSnippet{}
fails to compile if we use a new file, that hasn't imported
\KatlaSnippet{}.

\KatlaSnippet{}

\hypertarget{packages}{%
\section{Packages}\label{packages}}

We can add Idris 2 packages to the YAML metadata of the Markdown file,
using the \texttt{idris2-packages} key. For example, adding
\texttt{contrib} allows us to use the \texttt{Language.JSON} module.

\KatlaSnippet{}