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

Function fpMax

lean_py/z3/core.py:3403–3404  ·  view source on GitHub ↗
(a: FPRef, b: FPRef, ctx: Context | None = None)

Source from the content-addressed store, hash-verified

3401
3402
3403def fpMax(a: FPRef, b: FPRef, ctx: Context | None = None) -> FPRef:
3404 return _fp_op("fpMax", a, b)
3405
3406
3407# FP comparisons

Callers 2

test_fp_min_maxMethod · 0.90
test_maxMethod · 0.90

Calls 1

_fp_opFunction · 0.85

Tested by 2

test_fp_min_maxMethod · 0.72
test_maxMethod · 0.72