Function RealSort

lean_py/z3/core.py:230–231 · view source on GitHub ↗

()

Source from the content-addressed store, hash-verified

228
229
230	def RealSort() -> ArithSortRef:
231	return ArithSortRef(RealASTSort())
232
233
234	def DeclareSort(name: str) -> UninterpretedSortRef:

resolve_sortMethod · 0.90

test_sort_reprMethod · 0.90

test_expression_sortMethod · 0.90

test_domainMethod · 0.90

test_three_arg_functionMethod · 0.90

test_real_sort_nameMethod · 0.90

test_sort_kind_realMethod · 0.90

test_tuple_constructor_callMethod · 0.90

test_triple_sortMethod · 0.90

test_eq_different_sortMethod · 0.90

test_torealMethod · 0.90

__init__Method · 0.85

RealASTSortClass · 0.90

ArithSortRefClass · 0.85

test_sort_reprMethod · 0.72

test_expression_sortMethod · 0.72

test_domainMethod · 0.72

test_three_arg_functionMethod · 0.72

test_real_sort_nameMethod · 0.72

test_sort_kind_realMethod · 0.72

test_tuple_constructor_callMethod · 0.72

test_triple_sortMethod · 0.72

test_eq_different_sortMethod · 0.72

test_torealMethod · 0.72