pretty printerを実行する例

Here is an example.

import Lean.Elab.Command

open Lean Elab Command in
elab "format_me " cmd:command : command => do
  elabCommand cmd
  let fmt ← liftCoreM <| PrettyPrinter.ppCategory `command cmd
  let alternateString := fmt.pretty
  logInfo m!"The command looks like this:\n---\n{alternateString}\n---"

/--
info: The command looks like this:
---
example : True :=
  trivial
---
-/
#guard_msgs in
format_me
example : True := trivial  -- `cmd` carries information about this line

Start from the Lean pretty-printer example included in the issue body and locate where similar code examples are documented in the repository. Confirm the intended documentation location and surrounding format before adding or adapting the example. Done means the example is included in the appropriate documentation and renders or checks successfully with the project's documentation workflow.