coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] an update to Foundations

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Coq-Club Club <coq-club AT inria.fr>, homotopytypetheory AT googlegroups.com, Types list list <types-announce AT lists.seas.upenn.edu>, agda list <agda AT lists.chalmers.se>
Subject: [Coq-Club] an update to Foundations
Date: Sun, 6 Nov 2011 12:01:43 -0500

Hello,

I have posted an update to Foundations library at
https://github.com/vladimirias ;.

There is now basic rational arithmetic defined using set quotients of types
as well as an extended version of the abstract algebra files, including many
results on relations and some results on integral domains and ( geometric )
fields.

Vladimir.

[Coq-Club] an update to Foundations, Vladimir Voevodsky