Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: Simple example

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: Simple example


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page