kdrag.utils.open_binder_unhygienic

kdrag.utils.open_binder_unhygienic(lam: QuantifierRef) tuple[list[ExprRef], ExprRef]

Do not use this. Use open_binder. Opens a quantifier with unfresh variables.

>>> x = smt.Int("x")
>>> open_binder_unhygienic(smt.ForAll([x], x > 0))
([x], x > 0)
Parameters:

lam (QuantifierRef)

Return type:

tuple[list[ExprRef], ExprRef]