(cls, data: str)
| 403 | |
| 404 | @classmethod |
| 405 | def from_txt(cls, data: str) -> Theorem: |
| 406 | premises, conclusion = data.split(' => ') |
| 407 | premises = premises.split(', ') |
| 408 | conclusion = conclusion.split(', ') |
| 409 | return Theorem( |
| 410 | premise=[Construction.from_txt(p) for p in premises], |
| 411 | conclusion=[Construction.from_txt(c) for c in conclusion], |
| 412 | ) |
| 413 | |
| 414 | def __init__( |
| 415 | self, premise: list[Construction], conclusion: list[Construction] |