Function fpFPToFP

lean_py/z3/core.py:3490–3491

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

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


def fpRealToFP(rm: FPRMRef, a: ArithRef, sort: FPSortRef, ctx: Context | None = None) -> FPRef: