diff options
Diffstat (limited to 'sec/reducer.ltx')
| -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 |