doc-src/TutorialI/Types/numerics.tex
 changeset 11148 79aa2932b2d7 parent 10983 59961d32b1ae child 11161 166f7d87b37f
equal inserted replaced
11147:d848c6693185 11148:79aa2932b2d7
    75 \begin{warn}
    75 \begin{warn}
    76 Numeric literals are not constructors and therefore must not be used in
    76 Numeric literals are not constructors and therefore must not be used in
    77 patterns.  For example, this declaration is rejected:
    77 patterns.  For example, this declaration is rejected:
    78 \begin{isabelle}
    78 \begin{isabelle}
    79 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
    79 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
    80 h\ \#3\ =\ \#2\isanewline
    80 "h\ \#3\ =\ \#2"\isanewline
    81 h\ i\ \ =\ i
    81 "h\ i\ \ =\ i"
    82 \end{isabelle}
    82 \end{isabelle}
    83
    83
    84 You should use a conditional expression instead:
    84 You should use a conditional expression instead:
    85 \begin{isabelle}
    85 \begin{isabelle}
    86 "h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)"
    86 "h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)"