Zulip Chat Archive

Stream: general

Topic: solve each goal in "by" mode


Kenny Lau (Apr 19 2018 at 12:22):

In by mode, i.e. by xxx; yyy; zzz, is there a way to not apply the tactics to every goal?

Mario Carneiro (Apr 19 2018 at 12:24):

you can use seq_focus, i.e. xxx; [yyy, zzz], or use a big tactic block by { xxx, yyy, zzz }

Kenny Lau (Apr 19 2018 at 12:24):

aha

Kenny Lau (Apr 19 2018 at 12:25):

I was trying focus [yyy, zzz] but it failed

Kenny Lau (Apr 19 2018 at 12:25):

turns out you don't say focus

Kenny Lau (Apr 19 2018 at 12:25):

how would you write this?

by simp [reduce.step, h] at H; cases L; injections;
    [cc, { rw ← h_2, from list.suffix_append _ _ } ]

Mario Carneiro (Apr 19 2018 at 12:27):

begin
  simp [reduce.step, h] at H,
  cases L; injections, {cc},
  rw ← h_2,
  exact list.suffix_append _ _
end

Kenny Lau (Apr 19 2018 at 12:28):

but it's three lines longer, lol

Kenny Lau (Apr 19 2018 at 12:28):

four lines longer. i can't count

Mario Carneiro (Apr 19 2018 at 12:28):

If you have to represent complicated control flow, you probably shouldn't be using by

Mario Carneiro (Apr 19 2018 at 12:29):

at some point it's saving lines by just deleting newlines


Last updated: Dec 20 2023 at 11:08 UTC