Documentation
Lean
.
Language
.
Util
Search
return to top
source
Imports
Lean.CoreM
Lean.Elab.InfoTree
Lean.Language.Basic
Imported by
Lean
.
Language
.
SnapshotTree
.
trace
Lean
.
Language
.
SnapshotTree
.
trace
.
go
source
def
Lean
.
Language
.
SnapshotTree
.
trace
(s :
SnapshotTree
)
:
CoreM
Unit
Produces trace of given snapshot tree, synchronously waiting on all children.
Equations
s
.trace
=
Lean.Language.SnapshotTree.trace.go
none
s
Instances For
source
partial def
Lean
.
Language
.
SnapshotTree
.
trace
.
go
(range? :
Option
String.Range
)
(s :
SnapshotTree
)
:
CoreM
Unit