Documentation

Mathlib.Tactic.Trace

Defines the trace tactic. #

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.
Instances For