Just procrastinated so hard I set up a blog and wrote about linearity and erasure in Idris 2. https://www.type-driven.org.uk/edwinb/linearity-and-erasure-in-idris-2.html … I'm probably not going to make a habit of this...
Yes, it's part of unification - you could replace the True and False with _ and it would also be fine.
-
-
I will show my ignorance of Idris: if it doesn't work you can always provide a proof? (When there exist one)
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.