∀ (env : Lean.Environment) (messages : Lean.MessageLog) (scopes : List Lean.Elab.Command.Scope)
  (usedQuotCtxts : Lean.NameSet) (nextMacroScope maxRecDepth : ℕ) (ngen : Lean.NameGenerator)
  (auxDeclNGen : Lean.DeclNameGenerator) (infoState : Lean.Elab.InfoState) (traceState : Lean.TraceState)
  (snapshotTasks : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  sizeOf
      { env := env, messages := messages, scopes := scopes, usedQuotCtxts := usedQuotCtxts,
        nextMacroScope := nextMacroScope, maxRecDepth := maxRecDepth, ngen := ngen, auxDeclNGen := auxDeclNGen,
        infoState := infoState, traceState := traceState, snapshotTasks := snapshotTasks } =
    1 + sizeOf env + sizeOf messages + sizeOf scopes + sizeOf usedQuotCtxts + sizeOf nextMacroScope +
                sizeOf maxRecDepth +
              sizeOf ngen +
            sizeOf auxDeclNGen +
          sizeOf infoState +
        sizeOf traceState +
      sizeOf snapshotTasks