coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] RE: available context in refine 'holes'

From: "Kouskoulas, Yanni A." <Yanni.Kouskoulas AT jhuapl.edu>
To: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] RE: available context in refine 'holes'
Date: Sun, 11 Jan 2009 11:53:38 -0500
Accept-language: en-US
Acceptlanguage: en-US
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

In the my previous e-mail, I made a typo:

>The refine tactic puts me in a proof environment that asks me to prove
>"lprop tl", which is correct, but it will not
> include information in the context about how tl relates to lst, i.e., lst =
> h :: tl.

This should say "about how tl relates to i, i.e. i = h :: tl."

-Yanni

[Coq-Club] available context in refine 'holes', Kouskoulas, Yanni A.
- [Coq-Club] RE: available context in refine 'holes', Kouskoulas, Yanni A.
- Re: [Coq-Club] available context in refine 'holes', Adam Chlipala
  - RE: [Coq-Club] available context in refine 'holes', Kouskoulas, Yanni A.