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 do

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 if you like long form unedited videos about someone failing to program, you can see my struggles with Idris 2 here[1] [0] https://github.com/dspx-plcr/qtt https://github.com/dspx-plcr/qtt [1] https://www.youtube.com/playlist?list=PL5CIEWYHtEXommjLd_zOPgLVyQCdTEYfu https://www.youtube.com/playlist?list=PL5CIEWYHtEXommjLd_zOP...