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: 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




Archive powered by MHonArc 2.6.18.

Top of Page