Create a file called nats.agda with these lines: If you’d like, you can test to see if you’ve installed the Agda standard library correctly. Check if the Agda standard library was installed correctly To do so, add the path to plfa.agda-lib to AGDA_DIR/libraries and add plfa to AGDA_DIR/defaults, each on a line of their own. If you want to complete the exercises found in the courses folder, or to import modules from the book, you need to do this. It is possible to set up PLFA as an Agda library as well. More information about placing the standard libraries is available from the Library Management page of the Agda documentation. In AGDA_DIR, create a plain-text file called defaults containing just the line standard-library.This lets Agda know that an Agda library called standard-library is available. In AGDA_DIR, create a plain-text file called libraries containing the /path/to/standard-library.agda-lib. If the AGDA_DIR directory does not already exist, create it.On Windows, AGDA_DIR usually defaults to %AppData%\agda, where %AppData% usually defaults to C:\Users\USERNAME\AppData\Roaming. On UNIX and macOS, AGDA_DIR defaults to ~/.agda. You will need to create two configuration files in AGDA_DIR. Check to see that the file “standard-library.agda-lib” exists, and make a note of the path to this file. You’ll need the path where you installed the standard library. Git clone -branch v1.6 -depth 1 agda-stdlib # Remove `-depth 1` if you want the complete git history of the standard library.įinally, we need to let Agda know where to find the Agda standard library. For most versions of macOS, you can install these by running the following command: On macOS, you’ll need to install the XCode Command Line Tools. On macOS: Install the XCode Command Line Tools Therefore, it’s important to have the specific versions of Agda and the standard library shown above. Furthermore, Agda is under active development, so if you install the development version from the GitHub, you might find the developers have introduced changes which break the code here. If you are using a package manager, like Homebrew or Debian apt, the version of Agda available there may be out-of date. There are several versions of Agda and its standard library online. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems. PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. However, if you wish to interact with the code or complete the exercises, you need several things: You can read PLFA online without installing anything.
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. Archives
December 2022
Categories |