kdrag.theories.real

Functions

`abstract_arith`(t)	Z3 has difficult ematching over arithmetic expressions.
`rlemma`(thm[, by])
`sin_lower`(n, x)
`sqrt_bnd`(n)
`sqrt_lower`(n, x)
`sqrt_upper`(x, n)

Modules