|
|
|
|
|
|
by nbouscal
4172 days ago
|
|
|
I'm not an expert, but I wouldn't think so. To me, full dependent types just means you have pi and sigma types. I don't see anything fundamental about pi and sigma types that would prevent you from having bottom in your language, or from allowing users to define partial functions. |
|
|