From ae5667cfc743fd85816562b2b3ac3e7648715c73 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Tue, 27 Nov 2018 12:14:49 +0000 Subject: [PATCH] Added comment regarding PLFA as an Agda library --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 6035f1e2..9dcd85bc 100644 --- a/README.md +++ b/README.md @@ -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. 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