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

Method __add__

lean_py/z3/core.py:3886–3893  ·  view source on GitHub ↗
(self, other: SeqRef)

Source from the content-addressed store, hash-verified

3884 super().__init__(ast, sort, vars)
3885
3886 def __add__(self, other: SeqRef) -> SeqRef:
3887 if not isinstance(other, SeqRef):
3888 return NotImplemented
3889 return SeqRef(
3890 SeqConcatNode(self._ast, other._ast),
3891 self._sort, # type: ignore[arg-type]
3892 _merge(self._vars, other._vars),
3893 )
3894
3895 def __getitem__(self, idx: ArithRef | int) -> ExprRef:
3896 if isinstance(idx, int):

Callers

nothing calls this directly

Calls 3

SeqConcatNodeClass · 0.90
SeqRefClass · 0.85
_mergeFunction · 0.85

Tested by

no test coverage detected