Basic constructions on quantitative containers and quantitative polynomial functors, formalised in Idris2.
The main files are:
QCont.idr
- results on quantitative containersQPF.idr
- partial formalisation of the section on quantitative polynomial functorsExamples.idr
- contains a few examples - lists, natural numbers and binary trees.
Checked with Idris 2, version 0.5.1-9b2811f26.