@@ -268,8 +268,8 @@ can be used to calculate a return type:
268.. code-block:: idris
268.. code-block:: idris
270 mkSingle : (x : Bool) -> isSingleton x
270 mkSingle : (x : Bool) -> isSingleton x
271− mkSingle False = 0
271+ mkSingle True = 0
272− mkSingle True = []
272+ mkSingle False = []
274Or it can be used to have varying input types. The following function
274Or it can be used to have varying input types. The following function
275calculates either the sum of a list of ``Nat``, or returns the given
275calculates either the sum of a list of ``Nat``, or returns the given
@@ -278,9 +278,9 @@ calculates either the sum of a list of ``Nat``, or returns the given
278.. code-block:: idris
278.. code-block:: idris
280 sum : (single : Bool) -> isSingleton single -> Nat
280 sum : (single : Bool) -> isSingleton single -> Nat
281− sum False x = x
281+ sum True x = x
282− sum True [] = 0
282+ sum False [] = 0
283− sum True (x :: xs) = x + sum True xs
283+ sum False (x :: xs) = x + sum False xs