100 \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also |
100 \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also |
101 supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$} |
101 supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$} |
102 which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$ |
102 which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$ |
103 \isasymFun~$\tau$}. |
103 \isasymFun~$\tau$}. |
104 \item[type variables,]\indexbold{type variable}\indexbold{variable!type} |
104 \item[type variables,]\indexbold{type variable}\indexbold{variable!type} |
105 denoted by \isaindexbold{'a}, \isa{'b} etc., just like in ML. They give rise |
105 denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML. They give rise |
106 to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity |
106 to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity |
107 function. |
107 function. |
108 \end{description} |
108 \end{description} |
109 \begin{warn} |
109 \begin{warn} |
110 Types are extremely important because they prevent us from writing |
110 Types are extremely important because they prevent us from writing |
181 \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}. |
181 \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}. |
182 |
182 |
183 Despite type inference, it is sometimes necessary to attach explicit |
183 Despite type inference, it is sometimes necessary to attach explicit |
184 \textbf{type constraints}\indexbold{type constraint} to a term. The syntax is |
184 \textbf{type constraints}\indexbold{type constraint} to a term. The syntax is |
185 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that |
185 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that |
186 \ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed |
186 \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed |
187 in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as |
187 in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as |
188 \isa{(x < y)::nat}. The main reason for type constraints are overloaded |
188 \isa{(x < y)::nat}. The main reason for type constraints are overloaded |
189 functions like \isa{+}, \isa{*} and \isa{<}. See \S\ref{sec:overloading} for |
189 functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for |
190 a full discussion of overloading. |
190 a full discussion of overloading. |
191 |
191 |
192 \begin{warn} |
192 \begin{warn} |
193 In general, HOL's concrete syntax tries to follow the conventions of |
193 In general, HOL's concrete syntax tries to follow the conventions of |
194 functional programming and mathematics. Below we list the main rules that you |
194 functional programming and mathematics. Below we list the main rules that you |