by_contra + push_neg

Stream: new members

[Bhavik Mehta]

Is there a tactic which combines by_contra and push_neg? It seems like it would be fairly useful, maybe by_contra! to resemble contrapose!?

[Jalex Stark]

I wonder if someone with no tactic-writing experience can figure this out by inspecting the source code for by_contra, contrapose and contrapose!?

[Bhavik Mehta]

maybe this is the thing which finally gets me to learn how to write tactics

[Jalex Stark]

(where by "figure this out" i mean "write the tactic")

[Kevin Buzzard]

I think this is how Patrick started too -- he just wanted there to be some simple things which weren't there.

[Kenny Lau]

I also started like that but didn't really continue much

[Bhavik Mehta]

I wonder if there should be a tactic writing stream?

[Jalex Stark]

I have been waiting to start that until I had a sufficiently concrete question to ask