Zulip Chat Archive

Stream: new members

Topic: Why does my goal change?

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Aug 04 2018 at 10:04):


view this post on Zulip 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

view this post on Zulip 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