diff options
| -rw-r--r-- | sec/lang.ltx | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/sec/lang.ltx b/sec/lang.ltx index e3fe075..c94f388 100644 --- a/sec/lang.ltx +++ b/sec/lang.ltx @@ -214,7 +214,7 @@ such that \(\unroll~(\roll~t) = t\). The equational theory for \lang{} is shown in \cref{fig:lang-theory}. The equations for functions, products and sums are standard \(\beta\)-reductions. Reducing inductive types requires the -\mapkw{} operator, as folding a value requires folding on all -inductive components too. +\mapkw{} operator, as folding a value requires recursively folding on +all inductive components too. \end{document} |