idris-ct

idris-ct copied to clipboard

Convert to Idris 2

9

We will have to consider this at some point, so I thought it would be good to put this out here. coming from https://github.com/statebox/idris-stbx-core/issues/34

marcosh

build times

5

Building takes quite a long time and lately has been failing on my measly 2GB ram machine. Is there a way to have an idris project depend on a pre-compiled...

Jake-Gillberg

Build error with idris 1.3.2

2

When running `idris --build idris-ct.ipkg` (or `idris --checkpkg idris-ct.pkg`), the build fails on `CoLimits/CoProduct.lidr` with the following error : ``` Entering directory `./src' Type checking ./CoLimits/CoProduct.lidr ./CoLimits/CoProduct.lidr:83:5-97:48: | 83 |...

dwarfmaster

improve compilation speed for ProductCategory

4

this is slowing down the compilation of all the monoidal part of the library coming from https://github.com/statebox/idris-stbx-core/issues/32

marcosh

Add Limits.Product to build

1

I'm getting the following error on a clean rebuild without this somehow: ``` Type checking ./Limits/Product.lidr No ibc for Dual/DualCategory ```

clayrat

pedagogically adding some non trivial structure

1

Not sure if it fits here, but I was looking at this library and wanted to see how to, say, add the definition of 2-categories as a test case. Now...

nrolland

Generalize graph, rename old def to finite graph

1

clayrat

provide the setting for a formal proof of https://mathoverflow.net/questions/346529/the-convolution-of-comonads-is-a-comonad

marcosh

Define adjunctions

5

sjoerdvisscher

@andrek-sbox was there still work to be done to complete this?

marcosh