Draft tactic captures value of `have` #291

New issue

Open

opened 2025-08-23 22:07:45 -07:00 by aniva · 0 comments

aniva commented

2025-08-23 22:07:45 -07:00

Owner

This is from PyPantograph's unit tests:

    def test_load_sorry(self):
        server = Server()
        unit, = server.load_sorry("theorem mystery (p: Prop) : p → p := sorry", ignore_values=False)
        #self.assertIsNotNone(unit.goal_state, f"{unit.messages}")
        state0 = unit.goal_state
        self.assertEqual(state0.goals, [
            Goal(
                "_uniq.3",
                [Variable(name="p", t="Prop")],
                target="p → p",
            ),
        ])
        state1 = server.goal_tactic(state0, tactic="intro h")
        state2 = server.goal_tactic(state1, tactic="exact h")
        self.assertTrue(state2.is_solved)

        state1b = server.goal_tactic(state0, tactic=TacticDraft("by\nhave h1 : Or p p := sorry\nsorry"))
        self.assertEqual(state1b.goals, [
            Goal(
                "_uniq.17",
                [Variable(name="p", t="Prop")],
                target="p ∨ p",
            ),
            Goal(
                "_uniq.19",
                [
                    Variable(name="p", t="Prop"),
                    Variable(name="h1", t="p ∨ p", v="?m.17"),
                ],
                target="p → p",
            ),
        ])

Notice that the value for h1 is ?m.17.

This is from PyPantograph's unit tests: ```python def test_load_sorry(self): server = Server() unit, = server.load_sorry("theorem mystery (p: Prop) : p → p := sorry", ignore_values=False) #self.assertIsNotNone(unit.goal_state, f"{unit.messages}") state0 = unit.goal_state self.assertEqual(state0.goals, [ Goal( "_uniq.3", [Variable(name="p", t="Prop")], target="p → p", ), ]) state1 = server.goal_tactic(state0, tactic="intro h") state2 = server.goal_tactic(state1, tactic="exact h") self.assertTrue(state2.is_solved) state1b = server.goal_tactic(state0, tactic=TacticDraft("by\nhave h1 : Or p p := sorry\nsorry")) self.assertEqual(state1b.goals, [ Goal( "_uniq.17", [Variable(name="p", t="Prop")], target="p ∨ p", ), Goal( "_uniq.19", [ Variable(name="p", t="Prop"), Variable(name="h1", t="p ∨ p", v="?m.17"), ], target="p → p", ), ]) ``` Notice that the value for `h1` is `?m.17`.