Documentation

Lean.Language.Util

source
def Lean.Language.SnapshotTree.trace (s : Lean.Language.SnapshotTree) :
Lean.CoreM Unit

Produces trace of given snapshot tree, synchronously waiting on all children.

Instances For
    source
    partial def Lean.Language.SnapshotTree.trace.go (range? : Option String.Range) (s : Lean.Language.SnapshotTree) :
    Lean.CoreM Unit