Signed-off-by: Jim Pryor <profjim@jimpryor.net>
<pre><code>ω (\h \lst. (isempty lst) zero (add one ((h h) (extract-tail lst))))
</code></pre>
<pre><code>ω (\h \lst. (isempty lst) zero (add one ((h h) (extract-tail lst))))
</code></pre>
and this will indeed implement the recursive function we couldn't earlier figure out how to define.
In broad brush-strokes, `H` is half of the `get_length` function we're seeking, and `H` has the form:
and this will indeed implement the recursive function we couldn't earlier figure out how to define.
In broad brush-strokes, `H` is half of the `get_length` function we're seeking, and `H` has the form: