∀ (tacticCode : Lean.Syntax) (ctx : Lean.Elab.Term.SavedContext) (kind : Lean.Elab.Term.TacticMVarKind)
  (delayOnMVars : optParam Bool false),
  sizeOf (Lean.Elab.Term.SyntheticMVarKind.tactic tacticCode ctx kind delayOnMVars) =
    1 + sizeOf tacticCode + sizeOf ctx + sizeOf kind + sizeOf delayOnMVars