|
|
|
|
|
|
by Kutta
4446 days ago
|
|
|
You're not misunderstanding. In short, we should rightfully expect our dependent type checker to be sound, if not complete. Weaker, non-dependent type systems can have complete checkers though, see for example http://www.mpi-sws.org/~neelk/bidir.pdf |
|
|