Skip to Content.
Sympa Menu

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

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: Georgi Guninski <guninski AT guninski.com>
  • To: Adam Chlipala <adam AT chlipala.net>
  • 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: Fri, 20 May 2011 12:19:04 +0300
  • Header: best read with a sniffer
...and is the "anything" type as good as False - if i rename your original 
False to FalseO and define "anything" to be False is Coq expected to work 
(possibly after modifying some proofs a bit) ?

On Thu, May 19, 2011 at 11:41:55AM -0400, Adam Chlipala wrote:
> 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

Archive powered by MhonArc 2.6.16.

Top of Page