The Coq mailing list

[Mandy Martino <tesleft AT hotmail.com>]

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