coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

chronological Thread

From: Adam Chlipala <adam AT chlipala.net>
To: Georgi Guninski <guninski AT guninski.com>
Cc: coq-club AT inria.fr
Subject: Re: [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 11:41:55 -0400

Georgi Guninski wrote:

what is the formal definition of "empty"

A type [T] is empty if you can prove [T -> False].

Lemma l1: anything.
Proof.
constructor 1.
(* this passes without plug-ins *)

So would running [idtac]. The problem is that you haven't finished the proof. :P

[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