Zulip Chat Archive

Stream: mathlib4

Topic: control_laws_tac

Sky Wilshaw (Nov 30 2022 at 12:50):

Is there a port of control_laws_tac (or a similar tactic) into mathlib4 yet?

Jireh Loreaux (Nov 30 2022 at 13:16):

You can just write tactic scripts directly, like by intros; rfl

Sky Wilshaw (Nov 30 2022 at 13:17):

Thanks, I didn't realise that tactic was just a tactic script!

Last updated: May 02 2025 at 03:31 UTC