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

small fixes to Naturals

Browse source
This commit is contained in:
wadler 2018-03-18 20:14:52 -03:00
parent b58de9d80e
commit e1bb83225b
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Naturals.lagda
View file

@ -303,9 +303,9 @@ the terms `m + n` and `_+_ m n` are equivalent.
The definition has a base case and an inductive case, corresponding to
those for the natural numbers. The base case says that adding zero to
a number (`zero + n`) returns that number (`n`). The inductive case
says that adding the successor of a number to another number (`(suc m)
+ n`) returns the successor of adding the two numbers (`suc (m+n)`).
a number, `zero + n`, returns that number, `n`. The inductive case
says that adding the successor of a number to another number,
`(suc m) + n`, returns the successor of adding the two numbers, `suc (m+n)`.
We say we are using *pattern matching* when constructors appear on the
left-hand side of an equation.