equal
deleted
inserted
replaced
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)" |