Classical reasoning support #
Given that there exists an element satisfying p
, returns one such element.
This is a straightforward consequence of, and equivalent to, Classical.choice
.
See also choose_spec
, which asserts that the returned value has property p
.
Instances For
Instances For
All propositions are Decidable
.
Instances For
Instances For
Instances For
Equations
Instances For
the Hilbert epsilon Function