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
Will I just keep asking rhetorical questions and thus begin a new persona in a new social network?
He/him