Lean.Syntax →
  Array Lean.Expr →
    optParam (Option Lean.Syntax) none →
      optParam Bool false →
        optParam (Option String) none →
          optParam (Option Lean.Elab.Tactic.SavedState) none → optParam Bool true → Lean.Elab.Tactic.TacticM Unit