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