Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] which set of functions in coq defined algebra operation?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] which set of functions in coq defined algebra operation?


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page