idris-ct
idris-ct copied to clipboard
statebox
formally verified category theory library
Provide an easy interface to work with commutative diagrams, so that it is easy to compose them
at the moment the associator does not work for some mysterious reason. Find out why and fix it - issue on [idris-lang #4690](https://github.com/idris-lang/Idris-dev/issues/4690)
in https://github.com/jameshaydon/smproc there is defined a monoidal category. Integrate it with out definitions coming from https://github.com/statebox/idris-stbx-core/issues/30
Running `idris2 --build ./idris-ct.ipkg` does not seem to work: ``` ---> Building idris-ct Uncaught error: Error: Can't recognise token. "idris-ct.ipkg":3:1--3:2 1 | package idris-ct 2 | 3 | {- ^...
``` ---> Building idris-ct Executing: cd "/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/idris-ct-fbc7f633e0d86bfe5b56a2c4b9db6f780d59106d" && /usr/bin/make -j4 -w compare CC="/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/compwrap/cc/usr/bin/clang" CXX="/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/compwrap/cxx/usr/bin/clang++" OBJC="/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/compwrap/objc/usr/bin/clang" OBJCXX="/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/compwrap/objcxx/usr/bin/clang++" INSTALL="/usr/bin/install -c" make: Entering directory `/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/idris-ct-fbc7f633e0d86bfe5b56a2c4b9db6f780d59106d' idris2 fileDiff/FileDiff.idr -o compare Error: While processing right...
Building `lhs2tex` pulls in a lot of stuff, since their makefiles build apparently does not work anymore. This also means that on many platforms it will not build at all...