diff options
| -rw-r--r-- | sec/encoding.ltx | 8 |
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 |