@@ -402,8 +402,9 @@ names, ``n`` and ``a``, which are not declared explicitly. These are
402Implicit arguments, given in braces ``{}`` in the type declaration,
402Implicit arguments, given in braces ``{}`` in the type declaration,
403are not given in applications of ``index``; their values can be
403are not given in applications of ``index``; their values can be
404inferred from the types of the ``Fin n`` and ``Vect n a``
404inferred 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
405+arguments. Any name beginning with a lower case letter which appears
406+as a parameter or index in a
406−type declaration, but which is otherwise free, will be automatically
407+type declaration, but which is otherwise unbound, will be automatically
407bound as an implicit argument. Implicit arguments can still be given
408bound as an implicit argument. Implicit arguments can still be given
408explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
409explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
@@ -786,8 +787,8 @@ as “sigma types”:
787.. code-block:: idris
788.. code-block:: idris
789− data Sigma : (A : Type) -> (P : A -> Type) -> Type where
790+ data Sigma : (a : Type) -> (P : a -> Type) -> Type where
790− MkSigma : {P : A -> Type} -> (a : A) -> P a -> Sigma A P
791+ MkSigma : {P : A -> Type} -> (x : a) -> P x -> Sigma a P
792Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
793Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
793of a pair of A and P, where the name ``a`` can occur inside ``P``.
794of a pair of A and P, where the name ``a`` can occur inside ``P``.