Zulip Chat Archive

Stream: Is there code for X?

Topic: tactic from list of tactics

Kayla Thomas (Oct 29 2023 at 20:40):

How does one create a tactic from a list of tactics in Lean 4? In Lean 3 I had

meta def SC : tactic unit :=
`[apply proof_imp_deduct,
  apply prop_complete,
  unfold formula.is_tauto_prime,
  simp only [eval_not, eval_imp],
  tauto]

Timo Carlin-Burns (Oct 29 2023 at 20:43):

This thread may be useful for you

Kayla Thomas (Oct 29 2023 at 20:44):

Thank you.

Last updated: Dec 20 2023 at 11:08 UTC