michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

minor edits to Natural. End of work on Fri 29 Dec

Browse source
This commit is contained in:
wadler 2017-12-29 15:58:21 -02:00
parent 1bd1f19f52
commit 92efda2162
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Naturals.lagda
View file

@ -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 that. But now the other rule tells us that since `zero` was a natural
number yesterday, `suc zero` is a natural number today. number yesterday, `suc zero` is a natural number today.
-- on the second day, there are two natural numbers -- on the second day, there are two natural numbers
zero zero
suc zero suc zero
And we repeat the process again. Once more, one rule tells us what 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 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 `suc zero` and `suc (suc zero)` are natural numbers. We already knew about
the first of these, but the second is new. the first of these, but the second is new.
-- on the third day, there are three natural numbers -- on the third day, there are three natural numbers
zero zero
suc zero suc zero
suc (suc zero) suc (suc zero)
The process continues. On the *n*th day there will be *n* distinct 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 natural numbers. Note that in this way, we only talk about finite sets