Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] how to run this program to verify a simple function?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to run this program to verify a simple function?


Chronological Thread 
  • From: "John Wiegley" <johnw AT newartisans.com>
  • To: Mandy Martino <tesleft AT hotmail.com>
  • Cc: "coq-club\@inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] how to run this program to verify a simple function?
  • Date: Sat, 23 Jan 2016 11:58:21 -0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pa0-f47.google.com
  • Ironport-phdr: 9a23:MS2C+RPWMqxOgfJChpQl6mtUPXoX/o7sNwtQ0KIMzox0Kf/7rarrMEGX3/hxlliBBdydsKIazbOO7Ou5AzNIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niabro8KYOl8XzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IeezAcq85Vb1VCig9eyBwvZWz9EqLcQzaw3IaXnRetxNSHwnD61muQprqtib0qsJ93zWfNMzyC7szXGLx1apzTA7Uj3JNFTk59inoi8F/iK9K6lr1pRt/xZH8ZoyKPeBif7jUe8hcTm1ECJV/TStEV8meaIsJR9UAMOlcopi37w8Mqhu4GiGqCfzm0CNJnXbwxusx1OF3QlKO5xApA99b6Cecl97yLqpHFLntlKQ=
  • Organization: New Artisans LLC

>>>>> Mandy Martino
>>>>> <tesleft AT hotmail.com>
>>>>> writes:

> i have already been using 3.12.1, why still have error?

I'm not sure, but 3.12 and Coq 8.0 are very old versions. Is there any way to
upgrade to OCaml 4 and Coq 8.4pl6? Then I could try your code here, if it is
available online anywhere.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2



Archive powered by MHonArc 2.6.18.

Top of Page