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\ (x,\ y)\ =\ f\ z\ in\ (y,\ x)}\\ |
18 \isa{let\ (\mbox{x},\ \mbox{y})\ =\ \mbox{f}\ \mbox{z}\ in\ (\mbox{y},\ \mbox{x})}\\ |
19 \isa{case\ xs\ of\ []\ {\isasymRightarrow}\ 0\ |\ (x,\ y)\ \#\ zs\ {\isasymRightarrow}\ x\ +\ y} |
19 \isa{case\ \mbox{xs}\ of\ []\ {\isasymRightarrow}\ 0\ |\ (\mbox{x},\ \mbox{y})\ \#\ \mbox{zs}\ {\isasymRightarrow}\ \mbox{x}\ +\ \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: |