Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
Eq()
BoolSort()
Const()
Consts()
DeclareSort()
Exists()
ForAll()
FuncRef
Function()
IntSort()
RealSort()
arg()
codomain()
decl()
domains()
eq()
expr_kind()
func_kind()
get_id()
is_accessor()
is_app()
is_constructor()
is_func()
is_if()
is_neg()
is_power()
is_recognizer()
is_uninterp()
is_wf()
num_args()
register_well_formed()
sort()
sort_kind()
Python __eq__ resolution rules flips the order if y is a subclass of x. This function corrects that.
>>> IntVal(1) + IntVal(2) == IntVal(3) 3 == 1 + 2 >>> Eq(IntVal(1) + IntVal(2), IntVal(3)) 1 + 2 == 3