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

Function Float16

lean_py/z3/core.py:3239–3240  ·  view source on GitHub ↗
(ctx: Context | None = None)

Source from the content-addressed store, hash-verified

3237
3238
3239def Float16(ctx: Context | None = None) -> FPSortRef:
3240 return FPSort(5, 11)
3241
3242
3243def Float32(ctx: Context | None = None) -> FPSortRef:

Callers 1

test_float16Method · 0.90

Calls 1

FPSortFunction · 0.85

Tested by 1

test_float16Method · 0.72