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 users who like the study of programming languages, formal semantics, types, or linguistics.