Zulip Chat Archive

Stream: general

Topic: goal scope


view this post on Zulip Johan Commelin (Mar 28 2019 at 08:36):

Can a tactic escape the focused goals? I am trying to write a defer tactic. Intended use should be something like this:

example :  n, n > 0 :=
begin
  refine by defer k, _⟩,
  exact nat.zero_lt_one,
end

view this post on Zulip Johan Commelin (Mar 28 2019 at 08:37):

The idea would be that by defer k adds a goal k : ℕ to the main goal, and uses that to instantiate the existential.

view this post on Zulip Johan Commelin (Mar 28 2019 at 08:38):

But because it's written inside the ⟨by defer k, _⟩, it can't see the main goal.

view this post on Zulip Rob Lewis (Mar 28 2019 at 09:28):

No. I'm not even sure what you mean by "add a goal to the main goal," or that "main goal" is well defined. For this example, at least, you get the behavior you want with apply exists.intro.

view this post on Zulip Kevin Buzzard (Mar 28 2019 at 09:47):

Goals are just metavariables, right? Tactic mode is just displaying them to us in a convenient way. When more than one goal is focused I've seen tactics which operate on all of them.

existsi _ I think also does what you want. Not at Lean right now, don't know if use _ does too.


Last updated: May 08 2021 at 09:11 UTC