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: Thu, 19 May 2011 18:39:06 +0300
  • Header: best read with a sniffer
On Thu, May 19, 2011 at 10:19:26AM -0400, Adam Chlipala wrote:
> >"anything" appears not empty.
> 
> [anything_False] above establishes that [anything] is, in fact, empty.

what is the formal definition of "empty", can "empty" have constructors:

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



Archive powered by MhonArc 2.6.16.

Top of Page