coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] which set of functions in coq defined algebra operation?
- Date: Sat, 23 Jan 2016 08:52:33 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing.csail.mit.edu
- Ironport-phdr: 9a23:aRfbqR99DSaO7P9uRHKM819IXTAuvvDOBiVQ1KB90OIcTK2v8tzYMVDF4r011RmSDdudsqobwLeJ+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStCU1pzonL3ts7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCKD735UeWUSkwJBBwGNuBj2V5L6miDhv+t5niybIYv7Qa1iCmfq1LtiVBK90HRPDDU+6myC0sE=
Mandy, I think everyone on this mailing list is glad to welcome newcomers, but your questions (with their combination of detail and level of basic-ness) seem more suitable for a different forum, perhaps the #coq IRC channel on Freenode. I hope you don't mind taking them there instead. On 01/23/2016 12:07 AM, Mandy Martino
wrote:
Hi John,
i
find that it is suitable for ocaml, it seems ocaml
is the fastest way to redefine equality or
isomorphism.
Regards,
Martin
From: tesleft AT hotmail.com To: johnw AT newartisans.com CC: coq-club AT inria.fr Date: Sat, 23 Jan 2016 10:51:15 +0800 Subject: RE: [Coq-Club] which set of functions in coq defined algebra operation? Hi John,
i would like custom define
equi_trans ,
can coq allow to redefine this ?
how to do this custom ?
if not, how to Extraction Coq.Relations.Relation_Definitions
to a ML file or agda2 file?
Record equivalence : Prop :=
{ equiv_refl : reflexive;
equiv_trans : transitive;
equiv_sym : symmetric}.
Regards,
Martin
> From: johnw AT newartisans.com
> To: tesleft AT hotmail.com > CC: 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 > > >>>>> 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.