Fix 475--478.

1 files changed, 4 insertions, 4 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index a5eedf4..1db6720 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -138,10 +138,10 @@ let balanced n f = primrec n with
 \label{subsec:inductive-types}
 
 We use a modified heap encoding to encode regular types. We use a
-\(\mathsf{List}~\nat\)-indexed heap, but use naturals as pointers. The
-idea is that the heap index describes the path taken through the term
-to reach a particular entry, whilst the pointers describe the next
-step along the path.
+\((\mathsf{List}~\nat)\)-indexed heap, but use naturals as
+pointers. The idea is that the heap index describes the path taken
+through the term to reach a particular entry, whilst the pointers
+describe the next step along the path.
 
 We choose to use a heap encoding over another encoding strategy for the
 following reasons. Firstly, inductive types in \lang{} can contain higher-order