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]