Added comment regarding PLFA as an Agda library
This commit is contained in:
parent
8babe49f9f
commit
ae5667cfc7
1 changed files with 2 additions and 0 deletions
|
@ -27,6 +27,8 @@ or by downloading [the zip archive](https://github.com/plfa/plfa.github.io/archi
|
||||||
Finally, we need to let Agda know where to find the standard library.
|
Finally, we need to let Agda know where to find the standard library.
|
||||||
For this, you can follow the instructions [here](https://agda.readthedocs.io/en/latest/tools/package-system.html#example-using-the-standard-library).
|
For this, you can follow the instructions [here](https://agda.readthedocs.io/en/latest/tools/package-system.html#example-using-the-standard-library).
|
||||||
|
|
||||||
|
(PLFA is itself an Agda library, so if you wish to import modules from the book, you can set it up in a similar way.)
|
||||||
|
|
||||||
|
|
||||||
# Building the book
|
# Building the book
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue