diff options
Diffstat (limited to 'sec')
| -rw-r--r-- | sec/systemt.ltx | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/sec/systemt.ltx b/sec/systemt.ltx index 7881396..b50928c 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -281,16 +281,10 @@ diagramatically in \cref{fig:box-pointer:tree}. The recursive depth of the tree is three, as there are at most three nested constructors (e.g.\ the path from root to the value four). - -%% This encoding strategy is a crude approximation of a heap of memory. -%% Implementing this strategy requires choosing a (first-order) indexing type. Due -%% to G\"odel encodings, \nat{} is sufficient. In \cref{subsec:encode-inductive} we -%% use lists of naturals to better reflect the tree-like structure of inductive -%% values. - \TODO{ \begin{itemize} - \item describe with a box-and-pointer diagram + \item create box-and-pointer diagram + \item describe box-and-pointer diagram \item explain briefly how to fold and roll \end{itemize} } |