∀ (e : Lean.Expr) (omitTopForall : Bool),
  Lean.Elab.Command.NameGen.mkBaseNameCore.visit'✝ e omitTopForall =
    match e with
    | Lean.Expr.const name us => do
      modify fun st =>
          { seen := Lean.Elab.Command.NameGen.MkNameState.seen✝ st,
            consts := (Lean.Elab.Command.NameGen.MkNameState.consts✝ st).insert name }
      pure
          (match name.eraseMacroScopes with
          | pre.str str => str.capitalize
          | x => "")
    | f.app x =>
      (fun x1 x2 => x1 ++ x2) <$> Lean.Elab.Command.NameGen.mkBaseNameCore.visit✝ f <*>
        Lean.Elab.Command.NameGen.mkBaseNameCore.visit✝¹ x
    | Lean.Expr.forallE binderName ty body binderInfo => do
      let sty ← Lean.Elab.Command.NameGen.mkBaseNameCore.visit✝² ty
      if (omitTopForall && sty == "") = true then Lean.Elab.Command.NameGen.mkBaseNameCore.visit✝³ body true
        else (fun x => "Forall" ++ sty ++ x) <$> Lean.Elab.Command.NameGen.mkBaseNameCore.visit✝⁴ body
    | Lean.Expr.sort Lean.Level.zero => pure "Prop"
    | Lean.Expr.sort a.succ => pure "Type"
    | Lean.Expr.sort u => pure "Sort"
    | x => pure ""