diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 315286571..a29dcbfd8 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -577,6 +577,45 @@ in the list of subgoals remaining to prove. % \term\ will be kept. %\end{Variants} +\subsection{{\tt apply {\term} in {\ident}} +\tacindex{apply {\ldots} in}} + +This tactic applies to any goal. The argument {\term} is a term +well-formed in the local context and the argument {\ident} is an +hypothesis of the context. The tactic {\tt apply {\term} in {\ident}} +tries to match the conclusion of the type of {\ident} against a non +dependent premisses of the type of {\term}, trying them from right to +left. If it succeeds, the statement of hypothesis {\ident} is +replaced by the conclusion of the type of {\ident}. The tactic also +returns as many subgoals as the number of other non dependent premises +in the type of {\term} and of the non dependent premises of the type +of {\ident}. The tactic {\tt apply} relies on first-order +pattern-matching with dependent types. + +\begin{ErrMsgs} +\item \errindex{Statement without assumptions} + +This happens if the type of {\term} has no non dependent premise. + +\item \errindex{Unable to apply} + +This happens if the conclusion of {\ident} does not match any of the +non dependent premises of the type of {\term}. +\end{ErrMsgs} + +\begin{Variants} +\item {\tt apply \nelist{\term}{,} in {\ident}} + +This applies each of {\term} in sequence in {\ident}. + +\item {\tt apply \nelist{{\term} {\bindinglist}}{,} in {\ident}} + +This does the same but uses the bindings in each {\bindinglist} to +instanciate the parameters of the corresponding type of {\term} +(see syntax of bindings in Section~\ref{Binding-list}). + +\end{Variants} + \subsection{\tt generalize \term \tacindex{generalize} \label{generalize}} |