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

Method __lt__

lean_py/z3/core.py:722–727  ·  view source on GitHub ↗
(self, other: BitVecRef | int)

Source from the content-addressed store, hash-verified

720
721 # Comparisons (signed, matching z3py operator semantics)
722 def __lt__(self, other: BitVecRef | int) -> BoolRef:
723 other = _coerce_bv(other, self._sort)
724 return BoolRef(
725 BinOpNode(BinOp.SLT, self._ast, other._ast),
726 _merge(self._vars, other._vars),
727 )
728
729 def __le__(self, other: BitVecRef | int) -> BoolRef:
730 other = _coerce_bv(other, self._sort)

Callers

nothing calls this directly

Calls 4

BinOpNodeClass · 0.90
_coerce_bvFunction · 0.85
BoolRefClass · 0.85
_mergeFunction · 0.85

Tested by

no test coverage detected