diff options
| -rw-r--r-- | sec/systemt.ltx | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/sec/systemt.ltx b/sec/systemt.ltx index 309de0f..a1141ab 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -75,7 +75,8 @@ argument form \(\epsilon\) (the empty list), and the type \(\nat \to \nat \to All System~T types are inhabited.\@ \nat{} is inhabited by zero, and any function type is inhabited when its codomain is inhabited by -taking the constant function. +taking the constant function. \textcite{syst-sn} proves all System~T +terms are strongly normalising. \subsection{Strategies for Encoding Inductive Types}% \label{subsec:encoding-strategies} |