@@ -149,10 +149,12 @@ 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`` such as ``(S (S (S (S Z))))``,
153+ Idris displays it as ``4``.
154+ The result of ``plus (S (S Z)) (S (S Z))``
155+ is actually ``(S (S (S (S Z))))``
156+ which is the natural number ``4``.
157+ This can be checked at the Idris prompt:
156158
157159::
158160