∀ (funId : Lean.Ident) (ctorVal? : Option Lean.ConstructorVal) (explicit ellipsis : Bool)
  (paramDecls : Array (Lean.Name × Lean.BinderInfo)) (paramDeclIdx : ℕ) (namedArgs : Array Lean.Elab.Term.NamedArg)
  (usedNames : Std.HashSet Lean.Name) (args : List Lean.Elab.Term.Arg) (newArgs : Array Lean.Term),
  sizeOf
      { funId := funId, ctorVal? := ctorVal?, explicit := explicit, ellipsis := ellipsis, paramDecls := paramDecls,
        paramDeclIdx := paramDeclIdx, namedArgs := namedArgs, usedNames := usedNames, args := args,
        newArgs := newArgs } =
    1 + sizeOf funId + sizeOf ctorVal? + sizeOf explicit + sizeOf ellipsis + sizeOf paramDecls + sizeOf paramDeclIdx +
            sizeOf namedArgs +
          sizeOf usedNames +
        sizeOf args +
      sizeOf newArgs