diff options
| -rw-r--r-- | sec/systemt.ltx | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/sec/systemt.ltx b/sec/systemt.ltx index b534040..309de0f 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -66,12 +66,12 @@ of natural numbers. Types in System~T are usually presented as binary trees, with branches representing arrows and leaves being \(\nat\). An alternative presentation is \emph{argument -form}~\cite{DBLP:books/sp/LongleyN15}. Notice that all types can be -written in the form \(A_1 \to \cdots \to A_n \to \nat\) for some unique list of -argument types \(A_i\). We can therefore represent a type by its list -of arguments. For example, the type \(\nat\) has argument form \(\epsilon\) -(the empty list), and the type \(\nat \to \nat \to (\nat \to \nat) \to \nat\) -has argument form \([\epsilon, \epsilon, [\epsilon]]\). +form}~\cites{dialectica?}{DBLP:books/sp/LongleyN15}. Notice that all +types can be written in the form \(A_1 \to \cdots \to A_n \to \nat\) for some +unique list of argument types \(A_i\). We can therefore represent a +type by its list of arguments. For example, the type \(\nat\) has +argument form \(\epsilon\) (the empty list), and the type \(\nat \to \nat \to +(\nat \to \nat) \to \nat\) has argument form \([\epsilon, \epsilon, [\epsilon]]\). All System~T types are inhabited.\@ \nat{} is inhabited by zero, and any function type is inhabited when its codomain is inhabited by |