@edwinbrady watched your second Idris lecture yesterday. Just wondering, why de Bruijn indices rather than HOAS?
Replying to @milessabin
@milessabin at least for the resource language, it's easier to use dsl notation to change the scoping rules. Otherwise - just personal taste
12:44 AM - 15 Mar 2013
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.