Fail-closed checks for theorems advertised as verified #
#assert_standard_axioms accepts only a theorem declaration whose transitive
axioms are among Lean's three standard foundational axioms. In particular,
sorryAx, user axioms, and Lean.ofReduceBool are rejected.
Equations
- One or more equations did not get rendered due to their size.