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

Minor fix

Browse source
This commit is contained in:
Wen Kokke 2020-02-08 14:30:29 +00:00
parent 310ab57692
commit 84556ab62e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -242,7 +242,7 @@ 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 pragma `suc zero`, `2` as shorthand for `suc (suc zero)`, and so on. The pragma
must be given a previously declared type (in this case `ℕ`) with must be given a previously declared type (in this case `ℕ`) with
precisely two constructors, one with no arguments (in this case `zero`), precisely two constructors, one with no arguments (in this case `zero`),
and one with a single argument of the given type (in this case `succ`). and one with a single argument of the given type (in this case `suc`).
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