equal
deleted
inserted
replaced
14 example \isa{\isasymlambda(x,y,z).x+y+z} and |
14 example \isa{\isasymlambda(x,y,z).x+y+z} and |
15 \isa{\isasymlambda((x,y),z).x+y+z}. |
15 \isa{\isasymlambda((x,y),z).x+y+z}. |
16 In addition to explicit $\lambda$-abstractions, tuple patterns can be used in |
16 In addition to explicit $\lambda$-abstractions, tuple patterns can be used in |
17 most variable binding constructs. Typical examples are |
17 most variable binding constructs. Typical examples are |
18 \begin{quote} |
18 \begin{quote} |
19 \isa{let\ {\isacharparenleft}\mbox{x}{\isacharcomma}\ \mbox{y}{\isacharparenright}\ {\isacharequal}\ \mbox{f}\ \mbox{z}\ in\ {\isacharparenleft}\mbox{y}{\isacharcomma}\ \mbox{x}{\isacharparenright}}\\ |
19 \isa{let\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ f\ z\ in\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}}\\ |
20 \isa{case\ \mbox{xs}\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ {\isacharparenleft}\mbox{x}{\isacharcomma}\ \mbox{y}{\isacharparenright}\ {\isacharhash}\ \mbox{zs}\ {\isasymRightarrow}\ \mbox{x}\ {\isacharplus}\ \mbox{y}} |
20 \isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y} |
21 \end{quote} |
21 \end{quote} |
22 Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).% |
22 Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).% |
23 \end{isamarkuptext}% |
23 \end{isamarkuptext}% |
24 \end{isabellebody}% |
24 \end{isabellebody}% |
25 %%% Local Variables: |
25 %%% Local Variables: |