As usual Idris is super cool, the implications of using quantitative type theory are very well explained and interesting.
So has anyone used Idris 1 or 2 for anything? What did you think?
There was this thread a while back, and @yannbane is on lobsters:https://lobste.rs/s/ogez9q/game_pure_language_part_1_introduction
Only for learning type driven development, beyond that it seems a bit like it needs a lot more baking before that cake is fully ready for prime time.
Was super fun though, the type system will let you encode things in ways that I found hard/impossible in things like Haskell/Rust/etc….