3 ms·
> Dependent types doesn't explain Coq's requirement for pure, total functions. That's where you are wrong. Partial functions introduce the bottom value and the
by DanWaterworth 14y ago
> Dependent types doesn't explain Coq's requirement for pure, total functions.
That's where you are wrong. Partial functions introduce the bottom value and then you can 'prove' arbitrary incorrect things.
- Locke1689 14y agoI'm not sure what you're saying. I was saying that simply being dependently typed doesn't necessitate pure total functions. Obviously, these features can be considered either highly suggested or necessary for ITPs. There are a number of ways you can get around totality with dependent types.