Defines the trace tactic.

def Lean.Parser.Tactic.trace : ParserDescr

trace msg displays msg in the info view.

Extensions:

• msg can be a literal string, or a term that evaluates to a string.

Equations

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