diff options
| -rw-r--r-- | sec/reducer.ltx | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/sec/reducer.ltx b/sec/reducer.ltx index af90ad0..114647a 100644 --- a/sec/reducer.ltx +++ b/sec/reducer.ltx @@ -22,14 +22,12 @@ term simultaneously. As System~T is confluent and strongly normalising, complete development will converge on the normal form of the input term. -We define System~T terms as the inductive type in -\cref{lst:term-ty}. The compiler, detailed in \cref{M-sec:compiler} -makes a few small changes to the syntax to be more descriptive. Most -notably, products are indexed by labels instead of by position. For -example, the \verb|Primrec| constructor takes a product with three -components: the target, and the branches for zero and successor. As -\lang{} is simply typed, there is no way to enforce terms are -correctly typed nor correctly scoped. +We define System~T terms as the inductive type in \cref{lst:term-ty}. +We use the keyword \verb|data| to introduce a fixed point type. Sums +are given in square brackets and products in angle brackets. As +\lang{} is simply typed, there is no way to statically enforce terms +are correctly typed nor correctly scoped, but one can write scope and +type checkers within \lang{}. \begin{listing} \begin{verbatim} |