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

Address PR feedback — remove additional agda specifics

Browse source
This commit is contained in:
Zachary Brown 2020-02-06 17:04:02 -08:00
parent 25fbc53ecb
commit 310ab57692
1 changed files with 4 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
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 `succ`).
(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
@ -252,20 +251,6 @@ with `zero` and `suc` requires space proportional to _n_, whereas
representing it as an arbitrary-precision integer in Haskell only representing it as an arbitrary-precision integer in Haskell only
requires space proportional to the logarithm of _n_. requires space proportional to the logarithm of _n_.
Note that the data declaration must come _before_ the `BUILTIN` pragma,
as Agda will attempt to bind the given built-in to whatever name is given
in the pragma statement. As such, that name must be in scope relative to
the pragma. If you encounter a "Not in scope" error after adding the
pragma, this is likely the cause.
Complete definition with pragma:
```
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
```
## Imports ## Imports