coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Mandy Martino <tesleft AT hotmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] which set of functions in coq defined algebra operation?
- Date: Sat, 23 Jan 2016 09:53:31 +0800
- Authentication-results: mail3-smtp-sop.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-OMC1S13.hotmail.com
- Importance: Normal
- Ironport-phdr: 9a23:4MYOOhPxQxK+ltVzOsUl6mtUPXoX/o7sNwtQ0KIMzox0KPr7rarrMEGX3/hxlliBBdydsKIazbOO7eu7CSQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTpkbnqpdaIM01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvNa8/VPlTCCksG2Ez/szi8xfZB0Pb7XwFF24SjxBgAg7f7Ri8UI2n4QXgse8o/SCcMdy+aLkuRTWk6O8/VBLzjCoJKxY5933Sg810yqlcpUTy9FRE34fIbdTNZ7JFdaTHcIZCSA==
Hi
which set of functions in coq defined algebra operation from equality or congruence relation or equivalence relation?
i would like to extract them and run in agda2 and edit transitive axiom for testing a new algebra
Regards,
Martin
- [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.