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