Mastodon Feed
dysfun@treehouse.systems ("gaytabase") wrote:
one of my warmups for littlegem has been porting elaboration zoo to idris. except i have been trying things with it, to take advantage of dependent types (elabzoo is in haskell, where there are no dependent types).
one thing i thought would be nice and simple was indexing terms by the number of open binders and using de bruijn indexing.
spoiler: do not.