Data

class pantograph.data.CompilationUnit(i_begin: int, i_end: int, messages: list[str] = <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.TacticInvocation(before: str, after: str, tactic: str, used_constants: list[str])

One tactic invocation with the before/after goals extracted from Lean source code.