∀ (e : Lean.Expr) (omitTopForall : optParam Bool false),
  Lean.Elab.Command.NameGen.mkBaseNameCore.visit✝ e omitTopForall = do
    let __do_lift ← get
    if Std.HashSet.contains (Lean.Elab.Command.NameGen.MkNameState.seen✝ __do_lift) e = true then pure ""
      else do
        let s ← Lean.Elab.Command.NameGen.mkBaseNameCore.visit'✝ e omitTopForall
        modify fun st =>
            { seen := Std.HashSet.insert (Lean.Elab.Command.NameGen.MkNameState.seen✝¹ st) e,
              consts := Lean.Elab.Command.NameGen.MkNameState.consts✝ st }
        pure s