Manual/Tutorial/logic.tex

76 Indeed, terms of the logic have types similar to those of \ML{} expressions.
81 \paragraph{Syntax of \HOL\ types}
83 The types of \HOL{} terms form an \ML{} type called \ml{hol_type}.
84 Expressions having the form \ml{``: $\cdots$ ``} evaluate to logical types.
103 To try to minimise confusion between the logical types of \HOL{} terms and the \ML{} types of \ML{} expressions, the former will be referred to as \emph{object language types} and the latter as \emph{meta-language types}.
147 In order to understand the behaviour of the quotation parser, it is necessary to understand how the type checker infers types for the four basic term categories.
150 When a quotation is entered into \HOL{}, the type checking algorithm uses the types of constants to infer the types of variables in the same quotation.
183 If there is not enough contextually-determined type information to resolve the types of all variables in a quotation, then the system will guess different type variables for all the unconstrained variables.
187 Alternatively, it is possible to explicitly indicate the required types by using the notation \ml{``$\mathit{term}$:$\mathit{type}$``}, as illustrated below.
199 \paragraph{Function application types}
259 \paragraph{Function types}
261 Functions have types of the form \ml{$\sigma_1$->$\sigma_2$}, where $\sigma_1$ and $\sigma_2$ are the types of the domain and range of the function, respectively.
274 The session below illustrates the use of these constants as infixes; it also illustrates object language versus meta-language types.
1101 reflected in the various \ML{} types that the built-in tacticals have.