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

Function SeqFoldLeftI

lean_py/z3/core.py:3983–3990  ·  view source on GitHub ↗

Indexed left fold over sequence.

(f: FuncDeclRef, init: ExprRef, s: ExprRef)

Source from the content-addressed store, hash-verified

3981
3982
3983def SeqFoldLeftI(f: FuncDeclRef, init: ExprRef, s: ExprRef) -> ExprRef:
3984 """Indexed left fold over sequence."""
3985 merged = init._vars | s._vars | frozenset([(f._name, f._ast_sort)])
3986 return ExprRef(
3987 AppNode(_AstVar("seq.foldli"), (_AstVar(f._name), init._ast, s._ast)),
3988 init._sort,
3989 merged,
3990 )
3991
3992
3993# ---------------------------------------------------------------------------

Callers

nothing calls this directly

Calls 2

AppNodeClass · 0.90
ExprRefClass · 0.85

Tested by

no test coverage detected