|
|
|
|
|
|
by dwohnitmok
1615 days ago
|
|
|
> Type-checking is undecidable. This is only true if you allow non-total functions in your types, which most dependently-typed languages don't by default (i.e. the condition implied by your soundness condition). By default in e.g. both Idris and Agda type-checking is decidable. |
|
|