summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Wed, 17 Mar 2010 12:21:54 +0100 | |

changeset 35809 | 1ed86128316c |

parent 35808 | df56c1b1680f |

child 35810 | a50237ec0ecd |

child 35811 | 3939ca38f366 |

document "nitpick_choice_spec" attribute

--- a/doc-src/Nitpick/nitpick.tex Wed Mar 17 12:01:01 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Wed Mar 17 12:21:54 2010 +0100 @@ -2617,6 +2617,12 @@ where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an optional monotonic operator. The order of the assumptions is irrelevant. +\flushitem{\textit{nitpick\_choice\_spec}} + +\nopagebreak +This attribute specifies the (free-form) specification of a constant defined +using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command. + \end{itemize} When faced with a constant, Nitpick proceeds as follows: @@ -2629,7 +2635,12 @@ the constant is not empty, it uses these rules as the specification of the constant. -\item[3.] Otherwise, it looks up the definition of the constant: +\item[3.] Otherwise, if the constant was defined using the +\hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the +\textit{nitpick\_choice\_spec} set associated with the constant is not empty, it +uses these theorems as the specification of the constant. + +\item[4.] Otherwise, it looks up the definition of the constant: \begin{enum} \item[1.] If the \textit{nitpick\_def} set associated with the constant