Suppress field names with default values during delaboration

[leodemoura]

The following example

import Lean
open Lean.Meta
#check ({} : Context)

produces

{ config :=
    { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false,
      transparency := TransparencyMode.default, zetaNonDep := true, trackZeta := false, unificationHints := true,
      proofIrrelevance := true, assignSyntheticOpaque := false, ignoreLevelMVarDepth := true, offsetCnstrs := true,
      etaStruct := true },
  lctx :=
    { fvarIdToDecl :=
        { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
      decls :=
        { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)),
          tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0,
          shift := Std.PersistentArray.initShift, tailOff := 0 } },
  localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none }

It would be nice to have an option to disable fields that have default values when delaborating structure instances. This feature is relevant for the doc-gen4. See https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Basic.html#Lean.Meta.MetaM.run

[leodemoura]

@kha It would be really nice to have. It will also affect the InfoView.