From 980cd360c5e1594eca273165de83219c9260a4ac Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 25 Jun 2025 17:22:47 +0100 Subject: Fix 380--382. --- sec/lang.ltx | 4 ++-- 1 file 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} -- cgit v1.2.3