coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ian Lynagh <igloo AT earth.li>
- To: Adam Koprowski <adam.koprowski AT gmail.com>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] decluttering proofs
- Date: Wed, 24 Feb 2010 01:17:28 +0000
On Wed, Feb 24, 2010 at 12:39:19AM +0000, Ian Lynagh wrote:
> On Wed, Feb 24, 2010 at 12:54:43AM +0100, Adam Koprowski wrote:
> >
> > Below find my quick go at defining append in a more concise
> > way (starting with a replacement for your definition of Sequence).
>
> Thanks! Unfortunately, it doesn't seem to work for me. Here:
>
> > Inductive Sequence : forall (from to : NameSet.t) (contains : ThingSet.t),
> > Type :=
> > | Nil : forall `{t : NameSet.t, e [=] ThingSet.empty}, t --[e]-> t
> > | Cons : forall `{p : Patch from mid, s : Sequence mid to contains, e
> > [=]
> > (ThingSet.add (thingOf p) contains)}, from --[e]-> to
> > where "s --[ c ]-> t ":= (Sequence s t c).
>
> I get:
> Error: Unbound and ungeneralizable variable e
> on the first occurence of e (before the [=], on the Nil line).
>
> Any idea what's wrong? I have trunk 12801.
mattam has just told me on IRC that the answer is that:
Generalizable All Variables.
is now needed.
Thanks
Ian
- [Coq-Club] decluttering proofs, Ian Lynagh
- Re: [Coq-Club] decluttering proofs,
Adam Koprowski
- Re: [Coq-Club] decluttering proofs,
Ian Lynagh
- Re: [Coq-Club] decluttering proofs, Ian Lynagh
- Re: [Coq-Club] decluttering proofs, Ian Lynagh
- Re: [Coq-Club] decluttering proofs,
Ian Lynagh
- Re: [Coq-Club] decluttering proofs,
Adam Koprowski
Archive powered by MhonArc 2.6.16.