coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] defining functions on equivalence classes

From: Lawrence Paulson <lp15 AT cam.ac.uk>
To: pvs AT csl.sri.com, hol-info AT lists.sourceforge.net, coq-club AT pauillac.inria.fr, isabelle-users AT cl.cam.ac.uk
Cc: John Harrison <johnh AT ichips.intel.com>
Subject: [Coq-Club] defining functions on equivalence classes
Date: Mon, 22 Mar 2004 11:14:30 +0000
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

How frequently are quotient constructions used in formal proofs? I think John Harrison used one to construct the rationals, and there are a couple in Isabelle, but are there others? Also, are there any publications describing such proofs?

Larry Paulson

[Coq-Club] defining functions on equivalence classes, Lawrence Paulson
- [Coq-Club] Re: [Hol-info] defining functions on equivalence classes, Konrad Slind
- [Coq-Club] Re: defining functions on equivalence classes, Randy Pollack
- [Coq-Club] Re: [Hol-info] defining functions on equivalence classes, Rob Arthan
- <Possible follow-ups>
- [Coq-Club] defining functions on equivalence classes, Michael Norrish