Highlights for those not following:
- Idris2 written in Idris
- core language based on "Quantitative Type Theory" which allows explicit annotation of erased types, and linear types
- Default Chez Scheme Idris2 backend runs faster than default C Idris1 backend. 
https://twitter.com/edwinbrady/status/1148349263761629185 …
-
-
Oh boy
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.