• 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.
To find the state of this project's repository at the time of any of these versions, check out the tags.
CHANGES.md 30.9 KB