coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Robin Green <greenrd AT greenrd.org>
- To: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Re: Simple example
- Date: Sun, 22 Feb 2009 17:37:41 +0000
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Organization: Swansea University
On Sun, 22 Feb 2009 12:42:18 -0500
Adam Chlipala
<adamc AT hcoop.net>
wrote:
> If you want to reason about your (transparent) definitions after you
> finish writing them, then [refine] is likely to be much more helpful
> than [Program]. The latter will add all sorts of coercions "behind
> the scenes."
Yes, which can make Programs more concise. I find this helpful.
> The program you write will in general not be the
> Gallina term that you end up with, and it's that Gallina term that
> you'd need to prove things about.
True, but so what? You can still see the term, but there's no need to
put it in the source file.
--
Robin
- Re: [Coq-Club] Re: Simple example, Adam Koprowski
- Re: [Coq-Club] Re: Simple example,
Adam Chlipala
- Re: [Coq-Club] Re: Simple example, Robin Green
- Re: [Coq-Club] Re: Simple example,
Adam Chlipala
- Re: [Coq-Club] Re: Simple example,
Luke Palmer
- Re: [Coq-Club] Re: Simple example, Adam Chlipala
- Re: [Coq-Club] Re: Simple example,
Luke Palmer
- Re: [Coq-Club] Re: Simple example,
Adam Chlipala
- Re: [Coq-Club] Re: Simple example, Robin Green
- Re: [Coq-Club] Re: Simple example,
Adam Chlipala
Archive powered by MhonArc 2.6.16.