# [Agda] Writing a paper in Literate Agda

Alan Jeffrey ajeffrey at bell-labs.com
Thu Nov 28 03:16:48 CET 2013

Hi everyone,

I've just been writing a paper using Agda as the mechanical proof
assistant. Previously, I've just written an Agda file and then
summarized its content in the paper. This time I decided to try an
experiment of actually writing the paper in Literate Agda, so the
mathematics in the paper is actually what has been validated. On the
whole, the experiment was successful, and I thought I'd summarize some
of the steps I used.

First of all, I defined some Agda functions such as:

&_ : ∀ {α} {A : Set α} → A → A
& x = x

_\\ : ∀ {α} {A : Set α} → A → A
x \\ = x

and a TeX function |...| which sets mathematics in sans serif so that I
can control the layout and font of Agda code, for example:

\begin{code}
|idN|    : & |Nat| → |Nat| \\
|idN|(x) = & x
\end{code}

This works for definitions in a fixed universe, but not for universe
polymorphic definitions, since Setω isn't allowed in user code, so I
defined:

Member : ∀ {α} → (A : Set α) → A → Set
Member A x = ⊤
syntax Member A x = x ∶ A

which means you can write:

\begin{comment}
\begin{code}
|id| : ∀ {/α} → {/A : Set α} → /A → /A
\end{comment}
\end{code}
\begin{code}
%id-type : ∀ {α} → {A : Set α} →
|id| ∶ & A → A \\
%id-type = tt
|id|(x) = & x
\end{code}

Why the weird variable names, /α and /A? Well, sometimes you need to
give Agda hints about not-so-inferrable arguments, and you don't want
them showing up in the paper, so you write:

\begin{code}
%id-defn : ∀ {α} → {A : Set α} {x} →
|id|{/A = A}(x) ≡ x
%id-defn = refl
\end{code}

And then with the appropriate bit of LaTeX hackery we can make {/stuff}
disappear (OK there's probably an easier way to do this then messing
around with \futurelet, but hey, it works!):

{\global\futurelet\rbr\relax}
\def\gobbleRest{\futurelet\nextchar\gobbleRestOne}
\def\gobbleRestOne{\ifx\nextchar\rbr\else\expandafter\gobbleRestTwo\fi}
\def\gobbleRestTwo#1{\gobbleRest}
\catcode\/=\active
\def/{\gobbleRest}

So in the paper, this just appears as "id(x) ≡ x" (with the "id" in sans
serif).

Another trick was to define (as suggested by Martin Escardo):

★ : ∀ {/α} → Set (suc /α)
★ {/α} = Set /α

which means we can write:

\begin{code}
%type-in-type :
★ ∶ ★
%type-in-type = tt
\end{code}

and pretend that we're using type-in-type but actually have the real
development use level polymorphism.

Er that was about it, hope this is useful to someone else writing a
paper in Literate Agda!

A.
`

More information about the Agda mailing list