coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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] which set of functions in coq defined algebra operation?
- Date: Fri, 22 Jan 2016 18:18:12 -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-f50.google.com
- Ironport-phdr: 9a23:3MJvfRcXQq5nI+f1UaBj5VARlGMj4u6mDksu8pMizoh2WeGdxc+4bB7h7PlgxGXEQZ/co6odzbGG7ea5ATJLvcrJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipduKO1sD2Gb1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S45W2Mag1JtChLZ7Rf9FsPtvzD+u+Rh8CmdIcj/TLRyUjOnufRRRQfsmRsAYnQb92HRwvNxga1frQPr70h9xI7Sf6mTOeV3ZL/cZtocXixKWcMHBAJbBYbpJakID+xJAudVoI3wthFG+Rm5BQ+zLOXi1TZSmn7t1Kshle8mFFeVj0QbA9sSvSGM/53OP6AIXLXwlfGQwA==
- Organization: New Artisans LLC
>>>>> Mandy Martino
>>>>> <tesleft AT hotmail.com>
>>>>> writes:
> which set of functions in coq defined algebra operation from equality or
> congruence relation or equivalence relation?
Perhaps you are looking for?
https://coq.inria.fr/library/Coq.Relations.Relation_Definitions.html
https://coq.inria.fr/library/Coq.Classes.RelationClasses.html
I'm not entirely sure what you really want, though.
--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2
- [Coq-Club] which set of functions in coq defined algebra operation?, Mandy Martino, 01/23/2016
- Re: [Coq-Club] which set of functions in coq defined algebra operation?, John Wiegley, 01/23/2016
- RE: [Coq-Club] which set of functions in coq defined algebra operation?, Mandy Martino, 01/23/2016
- RE: [Coq-Club] which set of functions in coq defined algebra operation?, Mandy Martino, 01/23/2016
- Re: [Coq-Club] which set of functions in coq defined algebra operation?, Adam Chlipala, 01/23/2016
- RE: [Coq-Club] which set of functions in coq defined algebra operation?, Mandy Martino, 01/23/2016
- RE: [Coq-Club] which set of functions in coq defined algebra operation?, Mandy Martino, 01/23/2016
- Re: [Coq-Club] which set of functions in coq defined algebra operation?, John Wiegley, 01/23/2016
Archive powered by MHonArc 2.6.18.