Defines the trace tactic.

def Lean.Parser.Tactic.trace : ParserDescr

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