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?

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: Fri, 22 Jan 2016 17:48:17 -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-pf0-f170.google.com
Ironport-phdr: 9a23:LAyZKRFxQ3/bUwq4WW0cHJ1GYnF86YWxBRYc798ds5kLTJ74pcSwAkXT6L1XgUPTWs2DsrQf27SQ6vi+EjdQqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh770osWNKF4YzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IeezAcq85Vb1VCig9eyBwvZWz9EqLcQzaw3IaXnRetxNSHwnD61muQprqtib0qsJ93zWfNMzyC7szXGLx1apzTA7Uj3JNFTk59inoi8F/iK9K6lr1pRt/xZH8ZoyKPeBif7jUe8hcTm1ECJV/TStEV8meaIsJR9UAMOlcopi37w8Mqhu4GiGqCfzm0CNJnXbwxusx1OF3QlKO5xApA99b6Cecl97yLqpHFLntlKQ=
Organization: New Artisans LLC

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

> Error: The reference Z was not found in the current environment.

I'm not sure whether the course defines Z some place, but otherwise you should
just need:

Require Import ZArith.

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

[Coq-Club] how to run this program to verify a simple function?, Mandy Martino, 01/23/2016
- Re: [Coq-Club] how to run this program to verify a simple function?, John Wiegley, 01/23/2016
  - RE: [Coq-Club] how to run this program to verify a simple function?, Mandy Martino, 01/23/2016
    - RE: [Coq-Club] how to run this program to verify a simple function?, Mandy Martino, 01/23/2016
      - Re: [Coq-Club] how to run this program to verify a simple function?, John Wiegley, 01/23/2016
        
        RE: [Coq-Club] how to run this program to verify a simple function?, Mandy Martino, 01/23/2016
        
        RE: [Coq-Club] how to run this program to verify a simple function?, Mandy Martino, 01/23/2016
        
        Re: [Coq-Club] how to run this program to verify a simple function?, John Wiegley, 01/23/2016
        RE: [Coq-Club] how to run this program to verify a simple function?, Mandy Martino, 01/24/2016
        Re: [Coq-Club] how to run this program to verify a simple function?, Adam Chlipala, 01/24/2016