I did something similar recently in Idris 2, specifically to see how ergonomic using quantitative type theory is. My experience is it's quite a hassle, but I don't think that's beyond reproach. The repo is here[0], and…
I did something similar recently in Idris 2, specifically to see how ergonomic using quantitative type theory is. My experience is it's quite a hassle, but I don't think that's beyond reproach. The repo is here[0], and…