@@ -402,8 +402,9 @@ names, ``n`` and ``a``, which are not declared explicitly. These are
402402Implicit arguments, given in braces ``{}`` in the type declaration,
403403are not given in applications of ``index``; their values can be
404404inferred from the types of the ``Fin n`` and ``Vect n a``
405−arguments. Any name with a which appears as a parameter or index in a
406−type declaration, but which is otherwise free, will be automatically
405+arguments. Any name beginning with a lower case letter which appears
406+as a parameter or index in a
407+type declaration, but which is otherwise unbound, will be automatically
407408bound as an implicit argument. Implicit arguments can still be given
408409explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
409410example:
@@ -786,8 +787,8 @@ as “sigma types”:
786787
787788.. code-block:: idris
788789
789− data Sigma : (A : Type) -> (P : A -> Type) -> Type where
790− MkSigma : {P : A -> Type} -> (a : A) -> P a -> Sigma A P
790+ data Sigma : (a : Type) -> (P : a -> Type) -> Type where
791+ MkSigma : {P : A -> Type} -> (x : a) -> P x -> Sigma a P
791792
792793Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
793794of a pair of A and P, where the name ``a`` can occur inside ``P``.