Modularizing/generalizing tracing functions

Stream: lean4

[nrs]

I made the following functions while attempting to figure out what's happening in MutualDef.lean, but these seem horrible and there's most definitely a better, more general way to declare them. Should these be declared outside of the elab monads?

import Lean
open Lean

def traceInfo : SourceInfo -> Lean.Elab.Command.CommandElabM Unit
| .original leading pos trailing endpos => do
  dbg_trace ".original"
  dbg_trace "leading : Substring"
  dbg_trace leading
  dbg_trace "pos : String.Pos"
  dbg_trace pos
  dbg_trace "trailing : Substring"
  dbg_trace trailing
  dbg_trace "endpos : String.Pos"
  dbg_trace endpos
| .synthetic pos endpos canon => do
  dbg_trace ".synthetic"
  dbg_trace "pos : String.Pos"
  dbg_trace pos
  dbg_trace "endpos : String.Pos"
  dbg_trace endpos
  dbg_trace "canonical : Bool"
  dbg_trace canon
| .none => do
  dbg_trace "none"

def traceInfo' : SourceInfo -> Lean.Elab.Term.TermElabM Unit
| .original leading pos trailing endpos => do
  dbg_trace ".original"
  dbg_trace "leading : Substring"
  dbg_trace leading
  dbg_trace "pos : String.Pos"
  dbg_trace pos
  dbg_trace "trailing : Substring"
  dbg_trace trailing
  dbg_trace "endpos : String.Pos"
  dbg_trace endpos
| .synthetic pos endpos canon => do
  dbg_trace ".synthetic"
  dbg_trace "pos : String.Pos"
  dbg_trace pos
  dbg_trace "endpos : String.Pos"
  dbg_trace endpos
  dbg_trace "canonical : Bool"
  dbg_trace canon
| .none => do
  dbg_trace "none"

[nrs]

deriving instance Repr for SourceInfo
def traceInfox : SourceInfo -> CommandElabM Unit := fun s => do dbg_trace (repr s)

is a possibility. is this the usual approach? (edit: realized after the fact that SourceInfo already has a Repr instance .................)

edit2: but what about if we want to make a similar instance for, e.g., DefView? automatic deriving fails in that case. Is the standard procedure to just manually declare Repr instances?