From d9b5581e2111d85b4d547b47dc9940a792747627 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 23 Apr 2025 16:00:32 +0100 Subject: Split point in two. --- sec/systemt.ltx | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) (limited to 'sec') 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} } -- cgit v1.2.3