def Lean.Elab.InfoTree.foldInfo' {α : Type u_1} (init : α) (f : Lean.Elab.ContextInfo → Lean.Elab.InfoTree → α → α) : Lean.Elab.InfoTree → α

Like InfoTree.foldInfo, but also passes the whole node to f instead of just the head.

Equations

• Lean.Elab.InfoTree.foldInfo' init f = Lean.Elab.InfoTree.foldInfo'.go f none init

partial def Lean.Elab.InfoTree.foldInfo'.go {α : Type u_1} (f : Lean.Elab.ContextInfo → Lean.Elab.InfoTree → α → α) (ctx? : Option Lean.Elab.ContextInfo) (a : α) : Lean.Elab.InfoTree → α

foldInfo'.go is like foldInfo' but with an additional outer context parameter ctx?.