19 The datatype \tydx{list} introduces two |
19 The datatype \tydx{list} introduces two |
20 constructors \cdx{Nil} and \cdx{Cons}, the |
20 constructors \cdx{Nil} and \cdx{Cons}, the |
21 empty~list and the operator that adds an element to the front of a list. For |
21 empty~list and the operator that adds an element to the front of a list. For |
22 example, the term \isa{Cons True (Cons False Nil)} is a value of |
22 example, the term \isa{Cons True (Cons False Nil)} is a value of |
23 type \isa{bool\ list}, namely the list with the elements \isa{True} and |
23 type \isa{bool\ list}, namely the list with the elements \isa{True} and |
24 \isa{False}. Because this notation becomes unwieldy very quickly, the |
24 \isa{False}. Because this notation quickly becomes unwieldy, the |
25 datatype declaration is annotated with an alternative syntax: instead of |
25 datatype declaration is annotated with an alternative syntax: instead of |
26 \isa{Nil} and \isa{Cons x xs} we can write |
26 \isa{Nil} and \isa{Cons x xs} we can write |
27 \isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and |
27 \isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and |
28 \isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this |
28 \isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this |
29 alternative syntax is the standard syntax. Thus the list \isa{Cons True |
29 alternative syntax is the familiar one. Thus the list \isa{Cons True |
30 (Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation |
30 (Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation |
31 \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} |
31 \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} |
32 means that \isa{{\isacharhash}} associates to |
32 means that \isa{{\isacharhash}} associates to |
33 the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}} |
33 the right: the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}} |
34 and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}. |
34 and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}. |
35 The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}. |
35 The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}. |
36 |
36 |
37 \begin{warn} |
37 \begin{warn} |
38 Syntax annotations are a powerful but optional feature. You |
38 Syntax annotations are a powerful but optional feature. You |