Mathlib.Tactic.Trace
source
trace
Evaluates a term to a string (when possible), and prints it as a trace message.