@@ -268,8 +268,8 @@ can be used to calculate a return type:
268268.. code-block:: idris
269269
270270 mkSingle : (x : Bool) -> isSingleton x
271− mkSingle False = 0
272− mkSingle True = []
271+ mkSingle True = 0
272+ mkSingle False = []
273273
274274Or it can be used to have varying input types. The following function
275275calculates 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
278278.. code-block:: idris
279279
280280 sum : (single : Bool) -> isSingleton single -> Nat
281− sum False x = x
282− sum True [] = 0
283− sum True (x :: xs) = x + sum True xs
281+ sum True x = x
282+ sum False [] = 0
283+ sum False (x :: xs) = x + sum False xs
284284
285285Vectors
286286-------