Stream: new members
Topic: Why does my goal change?
Ali Sever (Aug 04 2018 at 10:03):
constructor my goal was
?m_1 ∉ A. Then I used
cases h with p hp, and my goal became
?m_1[_] ∉ A. What does that mean, and why does it even happen?
Kenny Lau (Aug 04 2018 at 10:04):
Mario Carneiro (Aug 04 2018 at 10:24):
That is a representation of a delayed abstraction. It means that the metavariable
?m_1 has been partially instantiated, although it still hasn't figured out what it should be yet
Kevin Buzzard (Aug 04 2018 at 11:35):
Ali I think it's an unwise idea in general to have metavariables in your goals. Presumably you have more than one goal at this point, and another goal is probably asking you what the metavariable is. You might want to fill in some earlier hole.
Last updated: May 14 2021 at 03:27 UTC