The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Georgi Guninski wrote:
> Can I use this inductive type in a fixpoint (without declaring variable that 
> will lead to an axiom) ?
>
> Inductive anything : Prop := d: (False->anything).
>    

Yes, you can certainly write a [Fixpoint] definition over this type.  It 
will have to be a degenerate fixpoint with no recursive calls, since 
your type definition is not recursive.

> can i make a fixpoint of the sort:
> Fixpoint fi1(a : True) : anything
>    

If you can, you've found a bug in Coq, since it can be proved that no 
function of that type exists.

Lemma anything_False : anything -> False.
  destruct 1; auto.
Qed.

Hint Immediate anything_False.

Goal ~(True -> anything).
  intuition.
Qed.

> "anything" appears not empty.
>    

[anything_False] above establishes that [anything] is, in fact, empty.