oh it's because I have to write that other thing that I'm too tired to write I'm procrastinating
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
Sometimes I do PL memes. Sometimes I forget I'm in my 30s. Gradual typing etc. Splabmate.