equal
deleted
inserted
replaced
2590 For predicates defined using the \textbf{inductive} or \textbf{coinductive} |
2590 For predicates defined using the \textbf{inductive} or \textbf{coinductive} |
2591 command, this corresponds to the \textit{intros} rules. The introduction rules |
2591 command, this corresponds to the \textit{intros} rules. The introduction rules |
2592 must be of the form |
2592 must be of the form |
2593 |
2593 |
2594 \qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\> |
2594 \qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\> |
2595 \ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk \,\Longrightarrow\, c\ u_1\ |
2595 \ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk$ \\ |
2596 \ldots\ u_n$, |
2596 \hbox{}\qquad ${\Longrightarrow}\;\, c\ u_1\ \ldots\ u_n$, |
2597 |
2597 |
2598 where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an |
2598 where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an |
2599 optional monotonic operator. The order of the assumptions is irrelevant. |
2599 optional monotonic operator. The order of the assumptions is irrelevant. |
2600 |
2600 |
2601 \flushitem{\textit{nitpick\_choice\_spec}} |
2601 \flushitem{\textit{nitpick\_choice\_spec}} |