A collection of type definitions for formal proofs in category theory.
A working installation of Idris. Instructions can be found in the Idris documentation.
For global installation use:
idris --install idrisCT.ipkg
from the root directory of the repo. For local installation simply copy the file Categories.idr into the root of your project (and add it to yourProject.ipkg if using the Atom editor for instance).
In either case include in your .idr file using
import Categories
shortly after declaring your module. (The file Test/TestCategories.idr is a simple example.)
Some initial examples:
At the moment just compile the files in the Test directory.
- The Idris Language.