@@ -149,10 +149,13 @@ Idris prompt:
149149
150150.. note::
151151
152− Idris automatically desugars the ``Nat`` representation into a
153− more human readable format. 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− checked at the Idris prompt:
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.
155+ The result of ``plus (S (S Z)) (S (S Z))``
156+ is actually ``(S (S (S (S Z))))``
157+ which is the natural number 4.
158+ This can be checked at the Idris prompt:
156159
157160::
158161