From a4c207c1ce32acadfb7cf6ee529c46b626362a76 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Tue, 18 Dec 2018 11:38:33 +0000 Subject: [PATCH] Revert "Removed reference to TSPL from README" This reverts commit 5187a4cc6dc82d3d8ff91f207d39bc7e14d0e3be. --- README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/README.md b/README.md index 93910eed..a1a7c592 100644 --- a/README.md +++ b/README.md @@ -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). 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. +(Note: Currently, `make build` also builds the exercises in the `tspl` folder, so this is not an optional step.) + # Building the book