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

Function fpRoundToIntegral

lean_py/z3/core.py:3523–3525  ·  view source on GitHub ↗

Round FP value to integral.

(rm: FPRMRef, a: FPRef, ctx: Context | None = None)

Source from the content-addressed store, hash-verified

3521
3522
3523def fpRoundToIntegral(rm: FPRMRef, a: FPRef, ctx: Context | None = None) -> FPRef:
3524 """Round FP value to integral."""
3525 return _fp_op("fpRoundToIntegral", rm, a)
3526
3527
3528def fpToIEEEBV(a: FPRef, ctx: Context | None = None) -> BitVecRef:

Callers

nothing calls this directly

Calls 1

_fp_opFunction · 0.85

Tested by

no test coverage detected