• 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.
FsetSum.v 11.1 KB