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

Merge pull request #463 from plfa/zachrbrown-dev

Browse source 
Minor changes to fix #460
This commit is contained in:
Wen Kokke 2020-02-08 14:32:04 +00:00 committed by GitHub
commit 1c06cd319d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/plfa/part1/Naturals.lagda.md
View file

@ -239,11 +239,10 @@ Including the line
``` ```
tells Agda that `ℕ` corresponds to the natural numbers, and hence one tells Agda that `ℕ` corresponds to the natural numbers, and hence one
is permitted to type `0` as shorthand for `zero`, `1` as shorthand for is permitted to type `0` as shorthand for `zero`, `1` as shorthand for
`suc zero`, `2` as shorthand for `suc (suc zero)`, and so on. The `suc zero`, `2` as shorthand for `suc (suc zero)`, and so on. The pragma
declaration is not permitted unless the type given has exactly two must be given a previously declared type (in this case `ℕ`) with
constructors, one with no arguments (corresponding to zero) and precisely two constructors, one with no arguments (in this case `zero`),
one with a single argument of the same type given in the pragma and one with a single argument of the given type (in this case `suc`).
(corresponding to successor).
As well as enabling the above shorthand, the pragma also enables a As well as enabling the above shorthand, the pragma also enables a
more efficient internal representation of naturals using the Haskell more efficient internal representation of naturals using the Haskell