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