From 6091a5191c4c480ba6cfdb1cf647d40f1c78a579 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 Apr 2024 13:32:29 -0700 Subject: [PATCH] fix: Conversion goals and value printing --- pantograph/expr.py | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/pantograph/expr.py b/pantograph/expr.py index 300ab82..8bbb338 100644 --- a/pantograph/expr.py +++ b/pantograph/expr.py @@ -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: