1 files changed, 35 insertions, 5 deletions
diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index 7c8834c..8babf3c 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -37,16 +37,46 @@ correctly typed nor correctly scoped.
   \begin{verbatim}
 data Term
   [ Var: Nat
-  , Zero: <>
-  , Suc: Term
-  , Primrec: <Zero: Term; Suc: Term, Target: Term>
-  , Abs: Term
-  , App: <Fun: Term, Arg: Term>
+  ; Zero: <>
+  ; Suc: Term
+  ; Primrec: <Zero: Term; Suc: Term, Target: Term>
+  ; Abs: Term
+  ; App: <Fun: Term, Arg: Term>
   ]
   \end{verbatim}
   \caption{Inductive type representing System~T terms.}\label{lst:term-ty}
 \end{listing}
 
+An example function is \verb|rename|, taking a term and a renaming
+function \verb|Nat -> Nat|, and updating all variables according to
+the renaming function. The program is in \cref{lst:rename}. We use
+\verb|~| as the syntax for \roll{} and \verb|foldcase| is syntactic
+sugar for performing a \foldkw{} whose body immediately pattern
+matches on the induction hypothesis. Recall that a fold fills the
+shape type with the motive. For example, for the \verb|App| branch,
+\verb|p| has type
+\verb|<Fun: (Nat -> Nat) -> Term; Arg: (Nat -> Nat) -> Term>|. As
+application doesn't bind any variables, we can pass the renaming
+\verb|f| to the inductive components without modification. For
+abstraction and primitive recursion, we have to lift the renaming
+function, corresponding to binding a variable.
+
+\begin{listing}
+  \begin{verbatim}
+let rename (t : Term) : (Nat -> Nat) -> Term =
+  foldcase t by
+    { Var n     => \f => ~(Var (f n))
+    ; Zero _    => \f => ~(Zero <>)
+    ; Suc r     => \f => ~(Suc (r f))
+    ; Primrec p => \f =>
+      ~(Primrec <Zero: p.Zero f; Suc: p.Suc (lift f); Target: p.Target f>)
+    ; Abs r     => \f => ~(Abs (r (lift f)))
+    ; App p     => \f => ~(App <Fun: p.Fun f; Arg: p.Arg f>)
+    }
+  \end{verbatim}
+  \caption{Implementation of term renaming.}\label{lst:rename}
+\end{listing}
+
 \TODO{
   \begin{itemize}
     \item show some example snippets