Defines the trace tactic.

ink

def Lean.Parser.Tactic.trace : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.