Data

Contents

Data#

class pantograph.data.CheckTrackResult(src_messages: list[pantograph.message.Message], dst_messages: list[pantograph.message.Message], failure: str | None = None)#

property feedback#: Feedback based on the dst

class pantograph.data.CompilationUnit(i_begin: int, i_end: int, messages: list[pantograph.message.Message] = <factory>, invocations: Optional[list[pantograph.data.TacticInvocation]] = None, goal_state: Optional[pantograph.expr.GoalState] = None, goal_src_boundaries: Optional[list[Tuple[int, int]]] = None, new_constants: Optional[list[str]] = None)#

class pantograph.data.SearchTarget(goal_state: pantograph.expr.GoalState)#

class pantograph.data.TacticInvocation(before: str, after: str, tactic: str, used_constants: list[str])#: One tactic invocation with the before/after goals extracted from Lean source code.