Function Exists

lean_py/z3/core.py:1386–1391

(
    vars: ExprRef | Sequence[ExprRef],
    body: BoolRef,
)

def Exists(
    vars: ExprRef | Sequence[ExprRef],
    body: BoolRef,
) -> QuantifierRef:
    vs = [vars] if isinstance(vars, ExprRef) else list(vars)
    return QuantifierRef("\u2203", vs, body)


# ---------------------------------------------------------------------------