diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/RefMan-tac.tex | 61 |
1 files changed, 43 insertions, 18 deletions
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 25e0f7aed..cb4abb22e 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -383,10 +383,6 @@ second-order pattern-matching problem into a first-order one. \tacindex{set} \tacindex{pose}} -\Warning V8 updating to do - -\medskip - This replaces {\term} by {\ident} in the conclusion or in the hypotheses of the current goal and adds the new definition {\ident {\tt :=} \term} to the local context. The default is to make this @@ -394,41 +390,70 @@ replacement only in the conclusion. \begin{Variants} -\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in *} +\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in *}\\ + {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |- *}\\ - This is equivalent to the above form but applies everywhere in the - goal (both in conclusion and hypotheses). + This behaves as above but substitutes {\term} + everywhere in the goal (both in conclusion and hypotheses). \item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |-} - This is equivalent to the above form but applies everywhere in the - hypotheses. + This behaves the same but substitutes {\term} in + the hypotheses only (not in the conclusion). \item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- *} - This is equivalent to the default behavior of {\tt set}. + This is equivalent to {\tt set ( } {\ident} {\tt :=} {\term} {\tt + )}, i.e. it substitutes {\term} in the conclusion only. \item {\tt set ( {\ident$_0$} {\tt :=} {\term} {\tt ) in} {\ident$_1$}} - This behaves the same but substitutes {\term} not in the goal but in + This behaves the same but substitutes {\term} only in the hypothesis named {\ident$_1$}. \item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in} {\ident$_1$} {\tt at} {\num$_1$} \dots\ {\num$_n$} -This notation allows to specify which occurrences of the hypothesis -named {\ident$_1$} (or the goal if {\ident$_1$} is the word {\tt - Goal}) should be substituted. The occurrences are numbered from left -to right. A negative occurrence number means an occurrence which -should not be substituted. +This notation allows to specify which occurrences of {\term} have to +be substituted in the hypothesis named {\ident$_1$}. The occurrences +are numbered from left to right and are meaningful on a pure +expression using no implicit argument, notation or coercion. A +negative occurrence number means an occurrence which should not be +substituted. As an exception of the left-to-right order, the +occurrences in the {\tt return} subexpression of a {\tt match} are +considered {\em before} the occurrences in the matched term. + +For expressions using notations, or hiding implicit arguments or +coercions, it is recommended to make explicit all occurrences in +order by using {\tt Set Printing All} (see +section~\ref{SetPrintingAll}). + +\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- * at} + {\num$_1$} \dots\ {\num$_n$} + +This allows to specify which occurrences of the conclusion are concerned. \item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in} {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$} It substitutes {\term} at occurrences {\num$_1^i$} \dots\ - {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. One of the {\ident}'s - may be the word {\tt Goal}. + {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. Each {\tt at} part is + optional. + +\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in} + {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots + {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$} + {\tt |- *} {\tt at} {\num$'_1$} \dots\ {\num$'_n$} + + This is the more general form which combines all the previous + possibilities. + +\item {\tt set } {\term} + + This behaves as {\tt set (} {\ident} := {\term} {\tt )} but {\ident} + is generated by {\Coq}. This variant is available for the + forms with {\tt in} too. \item {\tt pose ( {\ident} {\tt :=} {\term} {\tt )}} |