From d61a4c8bfab87a9589a30e45c800d2d6926156d0 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sat, 28 Oct 2023 10:44:52 +0000 Subject: [PATCH] Added usage notes --- README.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/README.md b/README.md index d4989da..2d9737f 100644 --- a/README.md +++ b/README.md @@ -24,3 +24,18 @@ So far the contributions are: ## TODO TODOs are found inside the literate agda files! + +## Usage +The project requires a new version of agda-categories (newer than some package managers ship), so the easiest way to use this project is via the provided nix flake, which fetches my fork of agda-categories that is guaranteed to work with this project. + +To use the project you just have to open a development shell: +```sh +nix develop . +``` +(this will take 20 - 30 minutes the first time, because it has to typecheck the agda-categories library) + +There is also a Makefile for compiling every module and generating the html documentation. + +``` +make +```