Open srid opened 2 years ago
Idris 2 is based on Quantitative Type Theory (QTT), a core language developed by Bob Atkey and Conor McBride. In practice, this means that every variable in Idris 2 has a quantity associated with it.
https://arxiv.org/pdf/2104.00480.pdf
Idris 2 is based on Quantitative Type Theory (QTT), a core language developed by Bob Atkey and Conor McBride. In practice, this means that every variable in Idris 2 has a quantity associated with it.
https://arxiv.org/pdf/2104.00480.pdf