diff options
| -rw-r--r-- | sec/encoding.ltx | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 9ffe418..19f2a73 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -320,12 +320,7 @@ lookup the index in the old list. We encode \(\mathsf{max}~f~t\) by primitive recursion on the length of the list \(t\). -\[\doprimrec{t.0}{\zero}{x}{(x.1 - f~x.0) + f~x.0}\] -We compute the binary maximum by performing a truncated subtraction -followed by an addition. These both have standard -encodings~\cref{add+sub}. Note that we use the inductive hypothesis on -the left of the subtraction so that a naive partial evaluator can -reduce the maximum of a singleton list to a single value. +\[\doprimrec{t.0}{\zero}{x}{f~x.0 \sqcup x.1}\] The final operator to encode is pattern matching. We achieve this by inspecting the length of the list to match. |