Add more examples of cost monoids - Githubissues

jonsterling / agda-calf

A cost-aware logical framework, embedded in Agda.

https://jonsterling.github.io/agda-calf/

Apache License 2.0

55 stars 2 forks source link

Add more examples of cost monoids #18

Closed HarrisonGrodin closed 1 year ago

HarrisonGrodin commented 3 years ago

[x] Remove IsCancellative requirement
[x] Add more examples of cost monoids:
- [x] ℕ⊔-CostMonoid
- [x] ℤ-CostMonoid
- [x] ℚ-CostMonoid
- [x] ResourceMonoid
- [x] List-CostMonoid
- [x] cm-×, for products of cost monoids
- [x] sequentialParCostMonoid, for turning a commutative cost monoid into a parallel cost monoid

HarrisonGrodin commented 1 year ago

That took a while! :slightly_smiling_face: