3 ms·
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 typ
by tadfisher 4y 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.