Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

  • Sylvain Dailler's avatar
    Add experimental coq realization for Fset and other Set theory · c5d97975
    Sylvain Dailler authored
    The underlying datastructure is not satisfying nor are the proofs but at
    least there is a quick simple realization. It uses ClassicalEpsilon axioms
    such as excluded middle, indefinite_description etc...
    Some theory realizations are very far from reality because the axiom
    characterization is small.
Cardinal.v 27.9 KB