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

Function IntSort

lean_py/z3/core.py:222–223  ·  view source on GitHub ↗
()

Source from the content-addressed store, hash-verified

220
221
222def IntSort() -> ArithSortRef:
223 return ArithSortRef(IntASTSort())
224
225
226def NatSort() -> ArithSortRef:

Callers 15

resolve_sortMethod · 0.90
test_function_declarationMethod · 0.90
test_function_applicationMethod · 0.90
test_function_congruenceMethod · 0.90
test_function_injectivity_patternMethod · 0.90
test_multi_arg_functionMethod · 0.90
test_function_bool_rangeMethod · 0.90
test_function_composition_proofMethod · 0.90
test_array_creationMethod · 0.90
test_select_storeMethod · 0.90
test_store_select_axiomMethod · 0.90
test_store_select_different_indexMethod · 0.90

Calls 2

IntASTSortClass · 0.90
ArithSortRefClass · 0.85

Tested by 15

test_function_declarationMethod · 0.72
test_function_applicationMethod · 0.72
test_function_congruenceMethod · 0.72
test_function_injectivity_patternMethod · 0.72
test_multi_arg_functionMethod · 0.72
test_function_bool_rangeMethod · 0.72
test_function_composition_proofMethod · 0.72
test_array_creationMethod · 0.72
test_select_storeMethod · 0.72
test_store_select_axiomMethod · 0.72
test_store_select_different_indexMethod · 0.72
test_constant_arrayMethod · 0.72