version 2.0: re-starting from scratch with a new data model.

daviddoret · Jul 27, 2024 · 3b1762d · 3b1762d
1 parent 1e97409
commit 3b1762d
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 25 deletions.
diff --git a/.idea/workspace.xml b/.idea/workspace.xml
diff --git a/src/punctilious/meta_theory_1.py b/src/punctilious/meta_theory_1.py
@@ -266,16 +266,17 @@ def theory_proves_proposition_external_algorithm(p: as1.Tupl | None = None, a: a
     t: as1.Theory = as1.coerce_theory(t=a[0], interpret_none_as_empty=False, canonical_conversion=False)
     p2: as1.Formula = as1.coerce_formula(phi=a[1])
     if as1.is_valid_proposition_in_theory_1(p=p2, t=t):
-        phi: as1.Formula = t | as1.get_connectives().proves | p
+        phi: as1.Formula = t | as1.get_connectives().proves | p2
         return phi
     else:
         raise u1.ApplicativeError(
-            msg='Blablabla',
+            msg='Proposition `p2` is not valid in theory `t`. '
+                'It follows that `t ⊢ p` cannot be derived.',
             code=None,
-            p=p,
-            a=a,
+            p2=p2,
             t=t,
-            p2=p2
+            a=a,
+            p=p
         )