coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] functions on equivalence classes

From: Larry Paulson <Larry.Paulson AT cl.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
Subject: [Coq-Club] functions on equivalence classes
Date: Fri, 09 Apr 2004 10:02:26 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: Computer Laboratory, University of Cambridge, England

I have updated the equivalence classes paper by adding a section on how to
impose equational constraints on a recursive datatype. Again, comments are
welcome.

http://www.cl.cam.ac.uk/users/lcp/papers/Reports/equivclasses.pdf

Larry Paulson

[Coq-Club] functions on equivalence classes, Larry Paulson