∀ {α : Type} [inst : SizeOf α] (toAttributeImplCore : Lean.AttributeImplCore)
  (getParam : Lean.Name → Lean.Syntax → Lean.AttrM α) (afterSet : Lean.Name → α → Lean.AttrM Unit)
  (preserveOrder : Bool) (filterExport : Lean.Environment → Lean.Name → α → Bool),
  sizeOf
      { toAttributeImplCore := toAttributeImplCore, getParam := getParam, afterSet := afterSet,
        preserveOrder := preserveOrder, filterExport := filterExport } =
    1 + sizeOf toAttributeImplCore + sizeOf preserveOrder