chore: missing docstring + style updates for String docs#10640

david-christiansen merged 1 commit intoleanprover:masterleanprover/lean4:masterfrom

david-christiansen:doc-typosdavid-christiansen/lean4:doc-typosCopy head branch name to clipboard