Zulip Chat Archive

Stream: general

Topic: list of tactics

Jakob von Raumer (Mar 20 2018 at 15:28):

Is there a tactic that allows me to give a list of tactics where each one solves one goal?

Simon Hudon (Mar 20 2018 at 15:30):

Yes try this: https://github.com/leanprover/lean/blob/master/library/init/meta/tactic.lean#L845-L847

Mario Carneiro (Mar 20 2018 at 15:33):

The interactive way to write this is tac; [tac1, tac2, tac3]

Simon Hudon (Mar 20 2018 at 15:39):

I should really stop assuming people are scripting when answering :stuck_out_tongue_closed_eyes:

Last updated: Aug 03 2023 at 10:10 UTC