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

Function Array

lean_py/z3/core.py:1093–1095  ·  view source on GitHub ↗
(name: str, domain: SortRef, range_sort: SortRef)

Source from the content-addressed store, hash-verified

1091
1092
1093def Array(name: str, domain: SortRef, range_sort: SortRef) -> ArrayRef:
1094 s = ArraySort(domain, range_sort)
1095 return ArrayRef(_AstVar(name), s, frozenset([(name, s._ast_sort)]))
1096
1097
1098def Const(name: str, sort: SortRef) -> ExprRef:

Callers 15

test_array_creationMethod · 0.90
test_select_storeMethod · 0.90
test_store_select_axiomMethod · 0.90
test_store_select_different_indexMethod · 0.90
test_array_getitem_syntaxMethod · 0.90
test_map_function_over_arrayMethod · 0.90
test_is_sort_typesMethod · 0.90
test_array_functional_updateMethod · 0.90
test_select_childrenMethod · 0.90
test_store_childrenMethod · 0.90
test_is_selectMethod · 0.90
test_is_storeMethod · 0.90

Calls 2

ArraySortFunction · 0.85
ArrayRefClass · 0.85

Tested by 15

test_array_creationMethod · 0.72
test_select_storeMethod · 0.72
test_store_select_axiomMethod · 0.72
test_store_select_different_indexMethod · 0.72
test_array_getitem_syntaxMethod · 0.72
test_map_function_over_arrayMethod · 0.72
test_is_sort_typesMethod · 0.72
test_array_functional_updateMethod · 0.72
test_select_childrenMethod · 0.72
test_store_childrenMethod · 0.72
test_is_selectMethod · 0.72
test_is_storeMethod · 0.72