Theorem, ptheoremn, more zf, real seqeunces

Author: philzook58

src/kdrag/tactics.py

@@ -584,6 +584,7 @@ def intros(self) -> smt.ExprRef | list[smt.ExprRef] | Goal:
         goalctx = self.top_goal()
         goal = goalctx.goal
         ctx = goalctx.ctx
+        # TODO: Let's remove this
         if isinstance(goal, smt.QuantifierRef) and goal.is_forall():
             return self.fixes()
         self.pop_goal()
@@ -625,7 +626,15 @@ def intros(self) -> smt.ExprRef | list[smt.ExprRef] | Goal:
             raise ValueError("Intros failed.")
 
     def assumes(self, hyp: smt.BoolRef):
+        """
+
+        >>> p,q = smt.Bools("p q")
+        >>> l = Lemma(smt.Implies(p, q))
+        >>> l.assumes(p)
+        [p] ?|= q
+        """
         goalctx = self.intros()
+        assert isinstance(goalctx, Goal)
         if goalctx.ctx[-1].eq(hyp):
             return goalctx
         else:

src/kdrag/theories/real/__init__.py

@@ -6,7 +6,7 @@
 
 import kdrag.smt as smt
 import kdrag.theories.set as set_
-from kdrag.smt import ForAll, Function
+from kdrag.smt import ForAll
 import kdrag as kd
 import kdrag.property as prop