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

Revert "Removed reference to TSPL from README"

Browse source 
This reverts commit 5187a4cc6d.
This commit is contained in:
Wen Kokke 2018-12-18 11:38:33 +00:00
parent db506e79b1
commit a4c207c1ce
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
README.md
View file

@ -31,8 +31,11 @@ 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).
It is possible to set up PLFA as an Agda library as well. It is possible to set up PLFA as an Agda library as well.
If you are trying to complete the exercises found in the `tspl` folder, or otherwise want to import modules from the book, you need to do this.
To do so, add the path to `plfa.agda-lib` to `~/.agda/libraries` and add `plfa` to `~/.agda/defaults`, both on lines of their own. To do so, add the path to `plfa.agda-lib` to `~/.agda/libraries` and add `plfa` to `~/.agda/defaults`, both on lines of their own.
(Note: Currently, `make build` also builds the exercises in the `tspl` folder, so this is not an optional step.)
# Building the book # Building the book