|
|
|
|
|
|
by tadfisher
1460 days ago
|
|
|
It also makes static checking undecidable in pathological cases. I know Idris has this problem as well; they work around it by skipping partial functions in types, so you end up with "total" and "partial" programs where only the former are completely typechecked proofs. |
|
|