diff options
Diffstat (limited to 'sec')
| -rw-r--r-- | sec/systemt.ltx | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/sec/systemt.ltx b/sec/systemt.ltx index 54ba5f2..e66f499 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -171,8 +171,8 @@ the fold. Below is the fold over binary trees. \mathsf{leaf}(n). f(n); \mathsf{branch}(x, y). g(x, y) } \coloneq - \dolet{ - go = \doprimrec*{t}{\arb}{h}{ + \dolet{go}*{ + \doprimrec*{t}{\arb}{h}{ \lambda i. \domatch*{i}{ \mathsf{leaf}(n). f(n); \mathsf{branch}(l, r). g(h(l), h(r))}} @@ -206,21 +206,18 @@ respectively, and then case split on this sum. We detail this in \cref{fig:churc \mathsf{leaf}(n). f(n); \mathsf{branch}(x,y). g(x, y) } \coloneq - \dolet[t]{ - \roll = \lambda x. \domatch*[t]{x}{ + \dolet[t]{\roll}*{ + \lambda x. \domatch*[t]{x}{ \mathsf{Left}(n). \mathsf{leaf}(n); - \mathsf{Right}(x, y). \mathsf{branch}(x, y) - } - }{ - x = \dofoldmatch*{t}{ + \mathsf{Right}(x, y). \mathsf{branch}(x, y)} + }{x}*{ + \dofoldmatch*{t}{ \mathsf{leaf}(n). \mathsf{Left}(n); - \mathsf{branch}(x, y). \mathsf{Right}(\roll~x, \roll~y) - } + \mathsf{branch}(x, y). \mathsf{Right}(\roll~x, \roll~y)} }*{ \domatch*{x}{ \mathsf{Left}(n). f(n); - \mathsf{Right}(x, y). g(x, y) - } + \mathsf{Right}(x, y). g(x, y)} } \] \caption{How to perform pattern matching on binary trees for Church encodings. |