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...
-
-
Replying to @edwinbrady
Is `getUnr`’s type and implementation written correctly? It appears alpha-equivalent to `getLin`, yet the semantics of the two functions are contrasted.
1 reply 0 retweets 0 likes
Replying to @mx00s
Thanks, fixed! I edited the text directly rather than pasting in the code, which always ends badly...
6:38 AM - 10 Jan 2020
0 replies
0 retweets
1 like
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.