18 lines
466 B
Python
18 lines
466 B
Python
from dataclasses import dataclass
|
|
|
|
@dataclass(frozen=True)
|
|
class TacticInvocation:
|
|
"""
|
|
One tactic invocation with the before/after goals extracted from Lean source
|
|
code.
|
|
"""
|
|
before: str
|
|
after: str
|
|
tactic: str
|
|
|
|
@staticmethod
|
|
def parse(payload: dict):
|
|
return TacticInvocation(before=payload["goalBefore"],
|
|
after=payload["goalAfter"],
|
|
tactic=payload["tactic"])
|