coq-functions-in-zfc

Functions in classical ZFC. This mostly repeats Guillaume Alexandre's contribution `zf', but in classical logic and with a different proof style. We start with a simple axiomatization of some flavor of ZFC (for example Werner's implementation of ZFC should provide a model). We develop some very basic things like pairs, functions, and a little bit about natural numbers, following the standard classical path.

opam install coq-functions-in-zfc.8.5.0
homepage
https://github.com/coq-contribs/functions-in-zfc
license
LGPL 2
bugs tracker
https://github.com/coq-contribs/functions-in-zfc/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/functions-in-zfc/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-functions-in-zfc/coq-functions-in-zfc.8.5.0