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

Method as_expr

lean_py/z3/tactic.py:61–66  ·  view source on GitHub ↗

Disjunction of sub-goal conjunctions (any sub-goal suffices).

(self)

Source from the content-addressed store, hash-verified

59 return self._subgoals[i]
60
61 def as_expr(self) -> BoolRef:
62 """Disjunction of sub-goal conjunctions (any sub-goal suffices)."""
63 if not self._subgoals:
64 return BoolVal(True) # proved
65 exprs = [g.as_expr() for g in self._subgoals]
66 return Or(*exprs)
67
68 def __repr__(self) -> str:
69 return f"ApplyResult({len(self._subgoals)} subgoal(s))"

Callers 1

Calls 3

BoolValFunction · 0.90
OrFunction · 0.90
as_exprMethod · 0.45

Tested by 1