summaryrefslogtreecommitdiff
path: root/src/CC/Thinning.idr
AgeCommit message (Collapse)Author
2023-03-26Add type checking.HEADmasterChloe Brown
Currently, there is Set in Set. Next step is to add universe levels.
2023-03-25Extract thinnings to a new module.Chloe Brown
Also make the interface more abstract, so more efficient representations can be swapped in with less cost.