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

Class IntNumRef

lean_py/z3/core.py:554–568  ·  view source on GitHub ↗

Integer numeral — concrete integer value with extraction methods.

Source from the content-addressed store, hash-verified

552
553
554class IntNumRef(ArithRef):
555 """Integer numeral — concrete integer value with extraction methods."""
556
557 __slots__ = ()
558
559 def as_long(self) -> int:
560 """Return the integer value as a Python int."""
561 if isinstance(self._ast, IntLit):
562 return self._ast.val
563 if isinstance(self._ast, NatLit):
564 return self._ast.val
565 raise TypeError("Not an integer literal")
566
567 def as_string(self) -> str:
568 return str(self.as_long())
569
570
571class RatNumRef(ArithRef):

Callers 4

numeratorMethod · 0.85
denominatorMethod · 0.85
IntValFunction · 0.85
NatValFunction · 0.85

Calls

no outgoing calls

Tested by

no test coverage detected