@@ -788,7 +788,7 @@ as “sigma types”:
788.. code-block:: idris
788.. code-block:: idris
790 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
790 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
791− MkSigma : {P : A -> Type} -> (x : a) -> P x -> Sigma a P
791+ MkSigma : {P : a -> Type} -> (x : a) -> P x -> Sigma a P
793Again, 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
794of 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``.