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

minor change to Naturals

Browse source
This commit is contained in:
wadler 2018-03-01 20:27:15 +01:00
parent e34252934f
commit 6e6531e7ae
1 changed files with 2 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Naturals.lagda
View file

@ -24,16 +24,8 @@ Everyone is familiar with the natural numbers:
...
and so on. We write `ℕ` for the *type* of natural numbers, and say that
`0`, `1`, `2`, `3`, and so on are *values* of type `ℕ`. In Agda,
we indicate this by writing
0 : ℕ
1 : ℕ
2 : ℕ
3 : ℕ
...
and so on.
`0`, `1`, `2`, `3`, and so on are *values* of type `ℕ`, indicated by
writing `0 : ℕ`, `1 : ℕ`, `2 : ℕ`, `3 : ℕ`, and so on.
The set of natural numbers is infinite, yet we can write down
its definition in just a few lines. Here is the definition