|
|
|
|
|
|
by dllthomas
4446 days ago
|
|
|
Fair point! I was wrong above - "Can a dependent type system catch all type errors at compile time?" Yes, so long as you're okay with rejecting some correctly typed programs! If you're not okay with that, then your type checker might not halt. Shame it's too late to add an addendum above... |
|
|