From 37148ba36483aec2ceaa32039f0fdce0f5648bc1 Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 18 Jul 2026 19:48:03 +0300 Subject: [PATCH] fix: call typeof(var) in type-tactic inconsistency errors Also say "nonzero" in IsNonzero instead of "positive". --- src/estimates/simp.py | 6 +++--- tests/test_all.py | 11 +++++++++++ 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/estimates/simp.py b/src/estimates/simp.py index b2e0186..6b1b7c8 100644 --- a/src/estimates/simp.py +++ b/src/estimates/simp.py @@ -220,7 +220,7 @@ def activate(self, state: ProofState) -> list[ProofState]: newvar = new_var("pos_real", name) else: raise ValueError( - f"INCONSISTENCY: {name}:{typeof} was somehow proven positive, which is impossible." + f"INCONSISTENCY: {name}:{typeof(var)} was somehow proven positive, which is impossible." ) print(f"{name} is now of type {typeof(newvar)}.") @@ -277,7 +277,7 @@ def activate(self, state: ProofState) -> list[ProofState]: newvar = new_var("nonneg_real", name) else: raise ValueError( - f"INCONSISTENCY: {name}:{typeof} was somehow proven nonnegative, which is impossible." + f"INCONSISTENCY: {name}:{typeof(var)} was somehow proven nonnegative, which is impossible." ) print(f"{name} is now of type {typeof(newvar)}.") @@ -334,7 +334,7 @@ def activate(self, state: ProofState) -> list[ProofState]: newvar = new_var("nonzero_real", name) else: raise ValueError( - f"INCONSISTENCY: {name}:{typeof} was somehow proven positive, which is impossible." + f"INCONSISTENCY: {name}:{typeof(var)} was somehow proven nonzero, which is impossible." ) print(f"{name} is now of type {typeof(newvar)}.") diff --git a/tests/test_all.py b/tests/test_all.py index 862b3ed..a453b2d 100644 --- a/tests/test_all.py +++ b/tests/test_all.py @@ -110,3 +110,14 @@ def test_subst_all_solution_reversed(self, capsys): def test_sympy_simplify_solution(self, capsys): sympy_simplify_solution() self.proof_complete(capsys) + + def test_type_tactic_inconsistency_messages(self): + """Inconsistency errors should call typeof(var), and IsNonzero should say nonzero.""" + import inspect + from estimates.simp import IsNonzero, IsPositive, IsNonnegative + src = inspect.getsource(IsNonzero.activate) + assert "typeof(var)" in src + assert "proven nonzero" in src + assert "proven positive" not in src + assert "typeof(var)" in inspect.getsource(IsPositive.activate) + assert "typeof(var)" in inspect.getsource(IsNonnegative.activate)