diff options
author | Chloe Brown <chloe.brown.00@outlook.com> | 2025-04-23 16:00:32 +0100 |
---|---|---|
committer | Chloe Brown <chloe.brown.00@outlook.com> | 2025-04-23 16:00:32 +0100 |
commit | d9b5581e2111d85b4d547b47dc9940a792747627 (patch) | |
tree | 03089ad73cbcec48a3401efc262f045de26d12f4 /sec | |
parent | 4353f331b5ab4af157f576f54b1cc79dd08abb12 (diff) |
Split point in two.
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} } |