@@ -405,13 +405,14 @@ index : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a
405405\useverb{vindeximpty}
406406
407407\noindent
408−Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are not given in
409−applications of \texttt{index}; their values can be inferred from the types of
410−the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name which appears as a parameter
411−or index in a type declaration, but which is otherwise free, will be automatically
412−bound as an implicit argument.
413−Implicit arguments can still be given explicitly in applications, using
414−\texttt{\{a=value\}} and \texttt{\{n=value\}}, for example:
408+Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are
409+not given in applications of \texttt{index}; their values can be inferred from
410+the types of the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name
411+with a \remph{lower case initial letter} which
412+appears as a parameter or index in a type declaration, but which is otherwise
413+free, will be automatically bound as an implicit argument. Implicit arguments
414+can still be given explicitly in applications, using \texttt{\{a=value\}} and
415+\texttt{\{n=value\}}, for example:
415416
416417\begin{SaveVerbatim}{vindexexp}
417418
@@ -922,7 +923,7 @@ Intermediate values can be calculated using \texttt{let} bindings:
922923
923924mirror : List a -> List a
924925mirror xs = let xs' = rev xs in
925− app xs xs'
926+ xs ++ xs'
926927
927928\end{SaveVerbatim}
928929\useverb{letb}