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