equal
deleted
inserted
replaced
527 Their inductive definition: |
527 Their inductive definition: |
528 |
528 |
529 |
529 |
530 \begin{textblock}{6}(2,7.5) |
530 \begin{textblock}{6}(2,7.5) |
531 \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l} |
531 \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l} |
532 \bl{$r$} & \bl{$::=$} & \bl{$\ZERO$} & null\\ |
532 \bl{$r$} & \bl{$::=$} & \bl{$\ZERO$} & nothing\\ |
533 & \bl{$\mid$} & \bl{$\ONE$} & empty string / \pcode{""} / $[]$\\ |
533 & \bl{$\mid$} & \bl{$\ONE$} & empty string / \pcode{""} / $[]$\\ |
534 & \bl{$\mid$} & \bl{$c$} & character\\ |
534 & \bl{$\mid$} & \bl{$c$} & character\\ |
535 & \bl{$\mid$} & \bl{$r_1 + r_2$} & alternative / choice\\ |
535 & \bl{$\mid$} & \bl{$r_1 + r_2$} & alternative / choice\\ |
536 & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\ |
536 & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\ |
537 & \bl{$\mid$} & \bl{$r^*$} & star (zero or more)\\ |
537 & \bl{$\mid$} & \bl{$r^*$} & star (zero or more)\\ |