Zulip Chat Archive

Stream: general

Topic: list of tactics


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 20 2018 at 15:33):

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

view this post on Zulip 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: May 12 2021 at 22:15 UTC