kdrag.theories.real.arb.flint_eq_ax_unsafe

kdrag.theories.real.arb.flint_eq_ax_unsafe(lhs, rhs)

This axiom schema is fishy, in that even if arb is implement correctly, this check does not assure the equality of the left and right hand side. but it is better than nothing.

>>> flint_eq_ax_unsafe(real.pi, 4*real.atan(1))
|- pi == 4*atan(1)
>>> flint_eq_ax_unsafe(smt.RealVal(0), real.sin(0))
|- 0 == sin(0)
>>> flint_eq_ax_unsafe(real.sin(3*real.pi/2), -1)
|- sin((3*pi)/2) == -1