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

Function fpInfinity

lean_py/z3/core.py:3538–3542  ·  view source on GitHub ↗

Generalized infinity constructor.

(sort: FPSortRef, negative: bool)

Source from the content-addressed store, hash-verified

3536
3537
3538def fpInfinity(sort: FPSortRef, negative: bool) -> FPNumRef:
3539 """Generalized infinity constructor."""
3540 if negative:
3541 return fpMinusInfinity(sort)
3542 return fpPlusInfinity(sort)
3543
3544
3545def fpZero(sort: FPSortRef, negative: bool) -> FPNumRef:

Callers

nothing calls this directly

Calls 2

fpMinusInfinityFunction · 0.85
fpPlusInfinityFunction · 0.85

Tested by

no test coverage detected