Open Seasawher opened 6 days ago
import Lean open Lean Elab Tactic elab "tada" : tactic => do let gs ← getUnsolvedGoals if gs.isEmpty then logInfo "Goals accomplished 🎉" else Term.reportUnsolvedGoals gs throwAbortTactic example : True := by trivial tada