equal
deleted
inserted
replaced
5 subsection{*Case expressions*} |
5 subsection{*Case expressions*} |
6 |
6 |
7 text{*\label{sec:case-expressions} |
7 text{*\label{sec:case-expressions} |
8 HOL also features \isaindexbold{case}-expressions for analyzing |
8 HOL also features \isaindexbold{case}-expressions for analyzing |
9 elements of a datatype. For example, |
9 elements of a datatype. For example, |
10 \begin{quote} |
|
11 @{term[display]"case xs of [] => 1 | y#ys => y"} |
10 @{term[display]"case xs of [] => 1 | y#ys => y"} |
12 \end{quote} |
|
13 evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if |
11 evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if |
14 @{term"xs"} is @{term"y#ys"}. (Since the result in both branches must be of |
12 @{term"xs"} is @{term"y#ys"}. (Since the result in both branches must be of |
15 the same type, it follows that @{term"y"} is of type @{typ"nat"} and hence |
13 the same type, it follows that @{term"y"} is of type @{typ"nat"} and hence |
16 that @{term"xs"} is of type @{typ"nat list"}.) |
14 that @{term"xs"} is of type @{typ"nat list"}.) |
17 |
15 |
32 error messages. |
30 error messages. |
33 \end{warn} |
31 \end{warn} |
34 \noindent |
32 \noindent |
35 Nested patterns can be simulated by nested @{text"case"}-expressions: instead |
33 Nested patterns can be simulated by nested @{text"case"}-expressions: instead |
36 of |
34 of |
37 % |
35 @{text[display]"case xs of [] => 1 | [x] => x | x # (y # zs) => y"} |
38 \begin{quote} |
|
39 @{text"case xs of [] => 1 | [x] => x | x#(y#zs) => y"} |
|
40 %~~~case~xs~of~[]~{\isasymRightarrow}~1~|~[x]~{\isasymRightarrow}~x~|~x~\#~y~\#~zs~{\isasymRightarrow}~y |
|
41 \end{quote} |
|
42 write |
36 write |
43 \begin{quote} |
|
44 @{term[display,eta_contract=false,margin=50]"case xs of [] => 1 | x#ys => (case ys of [] => x | y#zs => y)"} |
37 @{term[display,eta_contract=false,margin=50]"case xs of [] => 1 | x#ys => (case ys of [] => x | y#zs => y)"} |
45 \end{quote} |
|
46 |
38 |
47 Note that @{text"case"}-expressions may need to be enclosed in parentheses to |
39 Note that @{text"case"}-expressions may need to be enclosed in parentheses to |
48 indicate their scope |
40 indicate their scope |
49 *} |
41 *} |
50 |
42 |