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