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

Function FP

lean_py/z3/core.py:3255–3256  ·  view source on GitHub ↗
(name: str, fpsort: FPSortRef, ctx: Context | None = None)

Source from the content-addressed store, hash-verified

3253
3254
3255def FP(name: str, fpsort: FPSortRef, ctx: Context | None = None) -> FPRef:
3256 return FPRef(_AstVar(name), fpsort, frozenset([(name, fpsort._ast_sort)]))
3257
3258
3259def FPs(names: str, fpsort: FPSortRef, ctx: Context | None = None) -> tuple[FPRef, ...]:

Callers 15

test_fp_varMethod · 0.90
test_fp_negMethod · 0.90
test_fp_absMethod · 0.90
test_fp_sqrtMethod · 0.90
test_fp_predicatesMethod · 0.90
test_fp_to_realMethod · 0.90
test_fp_to_sbvMethod · 0.90
test_fp_to_ubvMethod · 0.90
test_fp_to_fpMethod · 0.90
test_fp_fp_to_fpMethod · 0.90
test_fp_sort_methodMethod · 0.90
test_fp_ebits_sbitsMethod · 0.90

Calls 1

FPRefClass · 0.85

Tested by 14

test_fp_varMethod · 0.72
test_fp_negMethod · 0.72
test_fp_absMethod · 0.72
test_fp_sqrtMethod · 0.72
test_fp_predicatesMethod · 0.72
test_fp_to_realMethod · 0.72
test_fp_to_sbvMethod · 0.72
test_fp_to_ubvMethod · 0.72
test_fp_to_fpMethod · 0.72
test_fp_fp_to_fpMethod · 0.72
test_fp_sort_methodMethod · 0.72
test_fp_ebits_sbitsMethod · 0.72