coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?

From: Georgi Guninski <guninski AT guninski.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?
Date: Thu, 19 May 2011 17:13:31 +0300
Header: best read with a sniffer

Can I use this inductive type in a fixpoint (without declaring variable that
will lead to an axiom) ?

Inductive anything : Prop := d: (False->anything).

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

"anything" appears not empty.

[Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?, Georgi Guninski
- Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?, Adam Chlipala
  - Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?, Georgi Guninski
    - Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?, Adam Chlipala
      - Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?, Lauri Alanko
        
        Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?, Daniel Schepler
        
        Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?, Pierre Courtieu
      - Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?, Georgi Guninski
        
        Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?, AUGER Cedric
      - Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?, Georgi Guninski
        
        Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?, AUGER Cedric