fix: Conversion goals and value printing
This commit is contained in:
parent
8658ec08e2
commit
6091a5191c
|
@ -28,7 +28,7 @@ class Variable:
|
|||
result = self.name if self.name else "_"
|
||||
result += f" : {self.t}"
|
||||
if self.v:
|
||||
result += f" = {self.v}"
|
||||
result += f" := {self.v}"
|
||||
return result
|
||||
|
||||
@dataclass(frozen=True)
|
||||
|
@ -36,6 +36,7 @@ class Goal:
|
|||
variables: list[Variable]
|
||||
target: Expr
|
||||
name: Optional[str] = None
|
||||
is_conversion: bool = False
|
||||
|
||||
@staticmethod
|
||||
def sentence(target: Expr) -> Self:
|
||||
|
@ -46,11 +47,13 @@ class Goal:
|
|||
name = payload.get("userName")
|
||||
variables = [Variable._parse(v) for v in payload["vars"]]
|
||||
target = parse_expr(payload["target"])
|
||||
return Goal(variables, target, name)
|
||||
is_conversion = payload["isConversion"]
|
||||
return Goal(variables, target, name, is_conversion)
|
||||
|
||||
def __str__(self):
|
||||
front = "|" if self.is_conversion else "⊢"
|
||||
return "\n".join(str(v) for v in self.variables) + \
|
||||
f"\n⊢ {self.target}"
|
||||
f"\n{front} {self.target}"
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class GoalState:
|
||||
|
|
Loading…
Reference in New Issue