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: Dec 20 2023 at 11:08 UTC