I don't kind of agree with your statement, since I earlier implemented a 80-line dependent lambda calculus [1]. I think dependent types make type checking a bit

I don't kind of agree with your statement, since I earlier implemented a 80-line dependent lambda calculus [1]. I think dependent types make type checking a bit more involved due to non-trivial type equality, but that's all about it. [1] https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196 https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c3...