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 18:16:18 -0800
Authentication-results: mail2-smtp-roc.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-f49.google.com
Ironport-phdr: 9a23:wKXo9hf0rLPHwKNnz6/Fcn/xlGMj4u6mDksu8pMizoh2WeGdxc+4bB7h7PlgxGXEQZ/co6odzbGG7ea5ATJLvcrJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipduKO1sD2Gb1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S45W2Mag1JtChLZ7Rf9FsPtvzD+u+Rh8CmdIcj/TLRyUjOnufRRRQfsmRsAYnQb92HRwvNxga1frQPr70h9xI7Sf6mTOeV3ZL/cZtocXixKWcMHBAJbBYbpJakID+xJAudVoI3wthFG+Rm5BQ+zLOXi1TZSmn7t1Kshle8mFFeVj0QbA9sSvSGM/53OP6AIXLXwlfGQwA==
Organization: New Artisans LLC

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

> is_empty_correct < destruct s; simpl; intuition.
> inversion_clear H0.
> elim H with z; auto.
> Error: Attempt to save an incomplete proof

Are you using the right version of Coq for this material? There seem to be a
lot of things going on, and I'm not sure what the underlying problem is from
this distance..

--
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