kdrag.rewrite.def_eq

kdrag.rewrite.def_eq(e1: ExprRef, e2: ExprRef, trace=None) → bool

A notion of computational equality. Unfold and simp.

>>> import kdrag.theories.nat as nat
>>> def_eq(nat.one + nat.one, nat.S(nat.S(nat.Z)))
True

Parameters:

• e1 (ExprRef)

• e2 (ExprRef)

Return type:

bool