## Stream: general

### Topic: goal scope

#### 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


#### 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.

#### 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.

#### 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.

#### 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