@@ -405,13 +405,14 @@ index : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a
405\useverb{vindeximpty}
405\useverb{vindeximpty}
408−Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are not given in
408+Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are
409−applications of \texttt{index}; their values can be inferred from the types of
409+not given in applications of \texttt{index}; their values can be inferred from
410−the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name which appears as a parameter
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
411−or index in a type declaration, but which is otherwise free, will be automatically
412+appears as a parameter or index in a type declaration, but which is otherwise
412−bound as an implicit argument.
413+free, will be automatically bound as an implicit argument. Implicit arguments
413−Implicit arguments can still be given explicitly in applications, using
414+can still be given explicitly in applications, using \texttt{\{a=value\}} and
414−\texttt{\{a=value\}} and \texttt{\{n=value\}}, for example:
415+\texttt{\{n=value\}}, for example:
416\begin{SaveVerbatim}{vindexexp}
417\begin{SaveVerbatim}{vindexexp}
@@ -922,7 +923,7 @@ Intermediate values can be calculated using \texttt{let} bindings:
923mirror : List a -> List a
924mirror : List a -> List a
924mirror xs = let xs' = rev xs in
925mirror xs = let xs' = rev xs in
925− app xs xs'
926+ xs ++ xs'
927\end{SaveVerbatim}
928\end{SaveVerbatim}
928\useverb{letb}
929\useverb{letb}