@@ -149,10 +149,12 @@ Idris prompt:
152− Idris automatically desugars the ``Nat`` representation into a
152+ When displaying an element of ``Nat`` such as ``(S (S (S (S Z))))``,
153+ Idris displays it as ``4``.
153− more human readable format. The result of ``plus (S (S Z)) (S (S Z))``
154+ The result of ``plus (S (S Z)) (S (S Z))``
154− is actually ``(S (S (S (S Z))))`` which is the Integer 4. This can be
155+ is actually ``(S (S (S (S Z))))``
156+ which is the natural number ``4``.
155− checked at the Idris prompt:
157+ This can be checked at the Idris prompt: