The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

But I can do that with all three:

Fixpoint f (n: nat) : n <> 0 -> nat.
  intro; exact 42. Defined.

Fixpoint f' (n: {m: nat | m <> 0}) : nat.
  exact 42. Defined.

Fixpoint f'' (n: nat) : nat + {n = 0}.
  exact (inleft 42). Defined.

 

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. When the type is forall n:nat, nat + { n=0 } then not only can it be called but it can return a natural number. Under the hypothesis that the side condition is decidable (which is the case for your examples), then forall n:nat, n<>0 -> nat is indeed isomorphic to something like forall n:nat, { _:nat | n<>0 } + { n = 0 }.

Not that there is anything wrong with your proposal, but it is a looser type, accepting more functions (for instance, despite appearances of the contrary, your f'' is a different function from f and f').