An axiomatisation of intuitionistic Zermelo-Fraenkel set theory

Authors:

Description:

Keywords:

README file:

La contribution ZF fournit une implantation des axiomes de
Zermelo-Fraenkel intuitioniste.  Elle contient :

- un repertoire src avec les sources (fich .v)
- un makefile pour la compilation et l'installation de la librairie.

Se reporter a INSTALL pour faire l'installation (il faut
essentiellement modifier deux variables dans makefile et src/makefile
pour indiquer le chemin de coqc). 

Source files:

• ZF.src.nothing
• ZF.src.ZFrelations
• ZF.src.axs_remplacement
• ZF.src.useful
• ZF.src.axs_fundation
• ZF.src.couples
• ZF.src.applications
• ZF.src.axs_paire
• ZF.src.MSetBasis
• ZF.src.axs_comprehension
• ZF.src.ZFbasis
• ZF.src.axs_extensionnalite
• ZF.src.axs_reunion
• ZF.src.axs_choice
• ZF.src.axs_parties