20 @{typ nat}, the type of natural numbers ($\mathbb{N}$), and @{typ int}, |
20 @{typ nat}, the type of natural numbers ($\mathbb{N}$), and @{typ int}, |
21 the type of mathematical integers ($\mathbb{Z}$). |
21 the type of mathematical integers ($\mathbb{Z}$). |
22 \item[type constructors,] |
22 \item[type constructors,] |
23 in particular @{text list}, the type of |
23 in particular @{text list}, the type of |
24 lists, and @{text set}, the type of sets. Type constructors are written |
24 lists, and @{text set}, the type of sets. Type constructors are written |
25 postfix, e.g.\ @{typ "nat list"} is the type of lists whose elements are |
25 postfix, i.e., after their arguments. For example, |
26 natural numbers. |
26 @{typ "nat list"} is the type of lists whose elements are natural numbers. |
27 \item[function types,] |
27 \item[function types,] |
28 denoted by @{text"\<Rightarrow>"}. |
28 denoted by @{text"\<Rightarrow>"}. |
29 \item[type variables,] |
29 \item[type variables,] |
30 denoted by @{typ 'a}, @{typ 'b} etc., just like in ML\@. |
30 denoted by @{typ 'a}, @{typ 'b} etc., just like in ML\@. |
31 \end{description} |
31 \end{description} |
39 @{text"\<tau>\<^sub>1"} then @{term"f t"} is a term of type @{text"\<tau>\<^sub>2"}. We write @{text "t :: \<tau>"} to mean that term @{text t} has type @{text \<tau>}. |
39 @{text"\<tau>\<^sub>1"} then @{term"f t"} is a term of type @{text"\<tau>\<^sub>2"}. We write @{text "t :: \<tau>"} to mean that term @{text t} has type @{text \<tau>}. |
40 |
40 |
41 \begin{warn} |
41 \begin{warn} |
42 There are many predefined infix symbols like @{text "+"} and @{text"\<le>"}. |
42 There are many predefined infix symbols like @{text "+"} and @{text"\<le>"}. |
43 The name of the corresponding binary function is @{term"op +"}, |
43 The name of the corresponding binary function is @{term"op +"}, |
44 not just @{text"+"}. That is, @{term"x + y"} is syntactic sugar for |
44 not just @{text"+"}. That is, @{term"x + y"} is nice surface syntax |
45 \noquotes{@{term[source]"op + x y"}}. |
45 (``syntactic sugar'') for \noquotes{@{term[source]"op + x y"}}. |
46 \end{warn} |
46 \end{warn} |
47 |
47 |
48 HOL also supports some basic constructs from functional programming: |
48 HOL also supports some basic constructs from functional programming: |
49 \begin{quote} |
49 \begin{quote} |
50 @{text "(if b then t\<^sub>1 else t\<^sub>2)"}\\ |
50 @{text "(if b then t\<^sub>1 else t\<^sub>2)"}\\ |