From 92efda21621415e1baec4341837af025c9268cb9 Mon Sep 17 00:00:00 2001 From: wadler Date: Fri, 29 Dec 2017 15:58:21 -0200 Subject: [PATCH] minor edits to Natural. End of work on Fri 29 Dec --- src/Naturals.lagda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 3ea3b0d7..7ee83a26 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -83,9 +83,9 @@ rule tells us that `zero` is a natural number, but we already knew that. But now the other rule tells us that since `zero` was a natural number yesterday, `suc zero` is a natural number today. - -- on the second day, there are two natural numbers - zero - suc zero + -- on the second day, there are two natural numbers + zero + suc zero And we repeat the process again. Once more, one rule tells us what we already knew, that `zero` is a natural number. And now the other rule @@ -93,10 +93,10 @@ tells us that since `zero` and `suc zero` are both natural numbers, then `suc zero` and `suc (suc zero)` are natural numbers. We already knew about the first of these, but the second is new. - -- on the third day, there are three natural numbers - zero - suc zero - suc (suc zero) + -- on the third day, there are three natural numbers + zero + suc zero + suc (suc zero) The process continues. On the *n*th day there will be *n* distinct natural numbers. Note that in this way, we only talk about finite sets