Zulip Chat Archive

Stream: new members

Topic: Why does my goal change?


Ali Sever (Aug 04 2018 at 10:03):

After using 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):

MWE

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: Dec 20 2023 at 11:08 UTC