Documentation
Mathlib
.
Tactic
.
Trace
Search
return to top
source
Imports
Init
Mathlib.Init
Lean.Meta.Eval
Lean.Elab.Tactic.ElabTerm
Imported by
Lean
.
Parser
.
Tactic
.
trace
Defines the
trace
tactic.
#
source
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.
Instances For