MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / AsArray

Function AsArray

lean_py/z3/core.py:2224–2231  ·  view source on GitHub ↗

Convert a function declaration to an array.

(f: FuncDeclRef)

Source from the content-addressed store, hash-verified

2222
2223
2224def AsArray(f: FuncDeclRef) -> ArrayRef:
2225 """Convert a function declaration to an array."""
2226 if len(f._domain) != 1:
2227 raise TypeError("AsArray requires a unary function")
2228 x = Const("__asarray_x", f._domain[0])
2229 lam = Lambda(x, f(x))
2230 result_sort = ArraySort(f._domain[0], f._range)
2231 return ArrayRef(lam._ast, result_sort, lam._vars)
2232
2233
2234# ---------------------------------------------------------------------------

Callers 3

test_as_arrayMethod · 0.90
test_as_array_basicMethod · 0.90

Calls 4

ConstFunction · 0.85
LambdaFunction · 0.85
ArraySortFunction · 0.85
ArrayRefClass · 0.85

Tested by 3

test_as_arrayMethod · 0.72
test_as_array_basicMethod · 0.72