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

Function is_real

lean_py/z3/core.py:2470–2471  ·  view source on GitHub ↗
(a: ExprRef)

Source from the content-addressed store, hash-verified

2468
2469
2470def is_real(a: ExprRef) -> bool:
2471 return isinstance(a._sort._ast_sort, RealASTSort)
2472
2473
2474def is_bool(a: ExprRef) -> bool:

Callers 15

test_toreal_astMethod · 0.90
test_is_sort_typesMethod · 0.90
test_is_sort_crossMethod · 0.90
test_fresh_real_sortMethod · 0.90
test_ratval_is_realMethod · 0.90
test_realval_intMethod · 0.90
test_torealMethod · 0.90
test_real_vectorMethod · 0.90
test_sqrtMethod · 0.90

Calls

no outgoing calls

Tested by 15

test_toreal_astMethod · 0.72
test_is_sort_typesMethod · 0.72
test_is_sort_crossMethod · 0.72
test_fresh_real_sortMethod · 0.72
test_ratval_is_realMethod · 0.72
test_realval_intMethod · 0.72
test_torealMethod · 0.72
test_real_vectorMethod · 0.72
test_sqrtMethod · 0.72