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

Function SeqFoldLeft

lean_py/z3/core.py:3973–3980  ·  view source on GitHub ↗

Left fold over sequence.

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

Source from the content-addressed store, hash-verified

3971
3972
3973def SeqFoldLeft(f: FuncDeclRef, init: ExprRef, s: ExprRef) -> ExprRef:
3974 """Left fold over sequence."""
3975 merged = init._vars | s._vars | frozenset([(f._name, f._ast_sort)])
3976 return ExprRef(
3977 AppNode(_AstVar("seq.foldl"), (_AstVar(f._name), init._ast, s._ast)),
3978 init._sort,
3979 merged,
3980 )
3981
3982
3983def SeqFoldLeftI(f: FuncDeclRef, init: ExprRef, s: ExprRef) -> ExprRef:

Callers

nothing calls this directly

Calls 2

AppNodeClass · 0.90
ExprRefClass · 0.85

Tested by

no test coverage detected