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

Method as_expr

lean_py/z3/tactic.py:34–36  ·  view source on GitHub ↗

Conjunction of all constraints.

(self)

Source from the content-addressed store, hash-verified

32 return len(self._constraints)
33
34 def as_expr(self) -> BoolRef:
35 """Conjunction of all constraints."""
36 return And(*self._constraints)
37
38 def __repr__(self) -> str:
39 return f"Goal({', '.join(repr(c) for c in self._constraints)})"

Callers 4

test_goal_as_exprMethod · 0.95
test_goal_as_exprMethod · 0.95
as_exprMethod · 0.45
applyMethod · 0.45

Calls 1

AndFunction · 0.90

Tested by 2

test_goal_as_exprMethod · 0.76
test_goal_as_exprMethod · 0.76