Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?


Chronological Thread 
  • From: Wolfram Kahl <kahl AT cas.mcmaster.ca>
  • To: "gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>
  • Cc: Adam Chlipala <adamc AT csail.mit.edu>, coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?
  • Date: Mon, 23 Jul 2012 12:40:57 -0400
On Mon, Jul 23, 2012 at 05:28:24PM +0100, gallais @ ensl.org wrote:
> "move into Prop" refers to moving away from a goal [A]
> (or [{ r | Some x = r}] in my example) which is in Type to
> a goal in Prop ([False]).
>
> There are a few cases where elimination of something
> in Prop when trying to build something in Type is allowed:
> http://coq.inria.fr/doc/Reference-Manual006.html#singleton

I think that clarifies it --- thank you very much!


Wolfram

Archive powered by MHonArc 2.6.18.

Top of Page