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