coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Mandy Martino <tesleft AT hotmail.com>
To: John Wiegley <johnw AT newartisans.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] which set of functions in coq defined algebra operation?
Date: Sat, 23 Jan 2016 10:51:15 +0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tesleft AT hotmail.com; spf=Pass smtp.mailfrom=tesleft AT hotmail.com; spf=None smtp.helo=postmaster AT BLU004-OMC4S17.hotmail.com
Importance: Normal
Ironport-phdr: 9a23:95/0DBOZF9rJhk1FzPcl6mtUPXoX/o7sNwtQ0KIMzox0KPvyrarrMEGX3/hxlliBBdydsKIazbOO7eu9ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTpkbnqpdaOO01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv+YJa6jxfrw5QLpEF3xmdjltvIy4/SXEGCmI5n1UbWQbnR5FEkCR7hb6WIjZtCblv/Bh2TKTO9awRrcxD2eM9aBuHTrhjisWfxsw6n3WjMs42L5WuxasqQBXw4nIZYiUMLx1eaaLLoBSfnZIQssED38JOYi7dYZaSrNZZes=

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