Function RealVector

lean_py/z3/core.py:1737–1739

Create a vector of ``sz`` real variables.

(prefix: str, sz: int)

def RealVector(prefix: str, sz: int) -> list[ArithRef]:
    """Create a vector of ``sz`` real variables."""
    return [Real(f"{prefix}__{i}") for i in range(sz)]


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