diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-25 17:22:47 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-25 17:22:47 +0100 |
| commit | 980cd360c5e1594eca273165de83219c9260a4ac (patch) | |
| tree | b596f65466b57bc8fe71bf884e6a5cdce0ff4143 | |
| parent | 4ae30cf7efb8358220510dc46a17e7ba99747d58 (diff) | |
Fix 380--382.
| -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} |