Quantitative types would have caught so many of my bugs over the years. I can't wait for this to become mainstream!
Good stuff! Thanks to all contributors, I'll have to start porting my libraries :p
I'm waiting for someone to update Brew which is currently at 1.3. Installing 2.0 is currently a bit of a faff.
Differences beteen Idris 1 and 2: [1]
There are a bunch of new features (scroll down to that in the doc) but the main thing seems to be moving to QTT (seems similar in theme to the bicolored calculus of constructions?) which allows explicit handling of erasure. Nice to see this as its the logical next step and consitent with Edwin Brady's larger project of making dependent types practical.
Note also the default target is Chez Scheme (Racket and Gambit supported) instead of C because its faster. Wouldn't it be funny to port it to Chicken?
[1]. https://idris2.readthedocs.io/en/latest/updates/updates.html