swap one goal

Stream: general

[Reid Barton]

Just something that occurred to me, but should swap when there's just one goal be an error? Or are there cases (probably involving things like ;?) where the current behavior (do nothing) is useful?

[Simon Hudon]

Are you asking because not having an error is giving you trouble?

[Reid Barton]

No actual trouble, I just had a swap that did nothing left over in my proof after a refactor.

[Simon Hudon]

So it can be kind of noisy

[Simon Hudon]

I also feel like it should be an error

[Simon Hudon]

If you're swapping the first two goals, you should know what the two goals correspond to, i.e. that they exist and they say something specific. Otherwise, you could do try { swap }

[Reid Barton]

I haven't really thought about it, but most tactics fail instead of doing nothing, on the premise that the user probably intended for something to happen.

[Reid Barton]

I'm using the slightly awkward specialize h _, swap, { ... }, repeatedly to provide a series of complicated arguments to a hypothesis

[Simon Hudon]

I don't see the connection between this last part and the rest

[Reid Barton]

I think what happened was that one of the { ... }s actually turned out to be trivial, so I moved it inline in place of the _

[Reid Barton]

then I had a swap that did nothing

[Simon Hudon]

I don't think I would say that we shouldn't let tactic do nothing. Sometimes, it's a natural generalization, like providing zero arguments to a function can sometimes make sense. Especially when you're trying to apply the same tactics multiple times

[Reid Barton]

but the whole construction feels kind of awkward in the first place

[Simon Hudon]

I see what you mean

[Simon Hudon]

It would make things better to get swap to fail

[Floris van Doorn]

I also think swap should fail on one goal. Someone who wants it can still run try {swap}.

[Mario Carneiro]

If swap did a rotation, then it would be reasonable for it to succeed on 1 goal

[Mario Carneiro]

but I think the present behavior is to move goal n to the front, in which case it should probably require that goal n exists