Function fpUnsignedToFP

lean_py/z3/core.py:3510–3515

(rm: FPRMRef, a: ExprRef, sort: FPSortRef, ctx: Context | None = None)

def fpUnsignedToFP(rm: FPRMRef, a: ExprRef, sort: FPSortRef, ctx: Context | None = None) -> FPRef:
    return FPRef(
        AppNode(_AstVar("fpUnsignedToFP"), (rm._ast, a._ast)),
        sort,
        _merge(rm._vars, a._vars),
    )


def fpNEQ(a: FPRef, b: FPRef, ctx: Context | None = None) -> BoolRef: