coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] fun <-> forall

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] fun <-> forall
Date: Mon, 30 Oct 2017 10:53:33 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f170.google.com
Ironport-phdr: 9a23:QxK3rRSymR7y6PqbFSvpBv1KVdpsv+yvbD5Q0YIujvd0So/mwa67YhCN2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnZBUin4YAFyP6H+HpPYp8WxzeG7vZPJMCtSgz/oSrfzKRiwsTLpt9VTqo9rN6o8zlOdqWNJZ+9SzH5kKFa7kBP158P295lmpXcD88k9/tJNBP2pN58zSqZVWWwr

On 2017-10-27 18:42, Samuel Gruetter wrote:
> this is a fun exercise :)
> Below is my solution, which, depending on taste, might be called simpler ;-)

Thanks, very nice!

Re: [Coq-Club] fun <-> forall, (continued)