Method __init__

lean_py/z3/core.py:576–580

(self, num: int, den: int)

    __slots__ = ("_num", "_den")

    def __init__(self, num: int, den: int) -> None:
        ast = BinOpNode(BinOp.DIV, ToRealNode(IntLit(num)), ToRealNode(IntLit(den)))
        super().__init__(ast, RealSort())
        self._num = num
        self._den = den

    def numerator(self) -> IntNumRef:
        return IntNumRef(IntLit(self._num), IntSort())