diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-26 17:41:46 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-26 17:41:46 +0100 |
| commit | 860938c1a4c912029c1ff9535805ff20ff7aa05b (patch) | |
| tree | 8eba2c244365d9ca627cedb985907230fe4be74b | |
| parent | 3fa012e5c3aa57fa785f354b2c1286446f8dbfb9 (diff) | |
Fix 815--522.
| -rw-r--r-- | sec/reducer.ltx | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/sec/reducer.ltx b/sec/reducer.ltx index 1e5757b..732154f 100644 --- a/sec/reducer.ltx +++ b/sec/reducer.ltx @@ -75,7 +75,7 @@ let rename (t : Term) : (Nat -> Nat) -> Term = The main driver in the reducer is the \verb|step| function, which performs a complete development of a term. We give its definition in -\cref{lst:step}. By induction, all terms within the \verb|foldcase| +\cref{lst:step}. By induction, all terms within the induction hypothesis have been completely developed. Most cases pass through their arguments unchanged: the only reductions for \(\suc~t\) happen within \(t\) for instance. The two interesting cases are \verb|Primrec| and |