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

Function MultiPattern

lean_py/z3/core.py:4072–4076  ·  view source on GitHub ↗

Quantifier multi-pattern.

(*args: ExprRef)

Source from the content-addressed store, hash-verified

4070
4071
4072def MultiPattern(*args: ExprRef) -> ExprRef:
4073 """Quantifier multi-pattern."""
4074 if args:
4075 return args[0]
4076 return BoolVal(True)
4077
4078
4079def DisjointSum(name: str, sorts: list[SortRef], ctx: Any = None) -> tuple:

Callers 2

test_multi_patternMethod · 0.90

Calls 1

BoolValFunction · 0.85

Tested by 2

test_multi_patternMethod · 0.72