The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Tue, Jul 16, 2013 at 9:50 AM, Arnaud Spiwack
<aspiwack AT lix.polytechnique.fr>
 wrote:

> Of course, but you misunderstood the sense of my remark. Your first 
> question was
> whether all three form were equivalent, and they aren't (as long as we 
> understand
> equivalent to mean isomorphic). In the case of  forall n:nat, n<>0 -> nat  
> the function
> cannot even be called if n=0.

Hm. Indeed. I was confusing the partiality of f and f' with them
having a Hoare-style precondition, as in: you can still call the
function if n = 0, but you get no guarantees about the output. But
you're right. They actually just have a restricted domain.

--
www.mhelvens.net