Real closed field number (not natively supported).
| 4625 | |
| 4626 | |
| 4627 | class RCFNum: |
| 4628 | """Real closed field number (not natively supported).""" |
| 4629 | |
| 4630 | def __init__(self, val: Any = 0) -> None: |
| 4631 | self._val = val |
| 4632 | |
| 4633 | def __repr__(self) -> str: |
| 4634 | return f"RCFNum({self._val})" |
| 4635 | |
| 4636 | def __add__(self, other: Any) -> RCFNum: |
| 4637 | return RCFNum(f"({self._val} + {other})") |
| 4638 | |
| 4639 | def __mul__(self, other: Any) -> RCFNum: |
| 4640 | return RCFNum(f"({self._val} * {other})") |
| 4641 | |
| 4642 | |
| 4643 | def Pi() -> ArithRef: |