diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 13aef43c76..206607911b 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1205,6 +1205,19 @@ When in a module, tells not to activate the implicit arguments of {\qualid} declared by this commands to contexts that requires the module. +\item {\tt \zeroone{Global {\sl |} Local} Implicit Arguments {\qualid} \sequence{[ \nelist{\possiblybracketedident}{} ]}{}} + +For names of constants, inductive types, constructors, lemmas which +can only be applied to a fixed number of arguments (this excludes for +instance constants whose type is polymorphic), multiple lists +of implicit arguments can be given. These lists must be of different +length, and, depending on the number of arguments {\qualid} is applied +to in practice, the longest applicable list of implicit arguments is +used to select which implicit arguments are inserted. + +For printing, the omitted arguments are the ones of the longest list +of implicit arguments of the sequence. + \end{Variants} \Example @@ -1228,6 +1241,8 @@ Fixpoint length (A:Type) (l:list A) : nat := Implicit Arguments map [A B]. Implicit Arguments length [[A]]. (* A has to be maximally inserted *) Check (fun l:list (list nat) => map length l). +Implicit Arguments map [A B] [A] []. +Check (fun l => map length l = map (list nat) nat length l). \end{coq_example} \Rem To know which are the implicit arguments of an object, use the command |