re: NbE for Sized Dependent Types
The reason size irrelevance seems like a hack to me is because I can't intuitively tell when I should be using relevant sizes and when I should be using irrelevant ones
Maybe once I understand it'll no longer seem like a hack
It was probably LexisNexis. Or Flash courses.
Much less 80,000
plz don't say 10,000
Will I just keep asking rhetorical questions and thus begin a new persona in a new social network?
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.