Additions to Lean.Elab.InfoTree.Main

def Lean.Elab.collectTryThisSuggestions (trees : PersistentArray InfoTree) : Array Meta.Tactic.TryThis.Suggestion

Collects all suggestions from all TryThisInfos in trees. Does not require context - works with context-free trees.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Elab.collectTryThisSuggestions.go (acc : Array Meta.Tactic.TryThis.Suggestion) : InfoTree → Array Meta.Tactic.TryThis.Suggestion

Traverses an InfoTree to collect TryThisInfo suggestions.

def Lean.Elab.InfoTree.findSomeM? {m : Type → Type} [Monad m] {α : Type} (f : ContextInfo → Info → PersistentArray InfoTree → m (Option α)) (t : InfoTree) (ctx? : Option ContextInfo := none) : m (Option α)

Finds the first result of ← f ctx info children which is some a, descending the tree from the top. Merges and updates contexts as it descends the tree.

f is only evaluated on nodes when some context is present. An initial context should be provided via the ctx? argument if invoking findSomeM? during a larger traversal of the infotree. A failure to provide ctx? := some ctx when t is not the outermost InfoTree is thus likely to cause findSomeM? to always return none.

Equations

• Lean.Elab.InfoTree.findSomeM? f t ctx? = Lean.Elab.InfoTree.findSomeM?.go f ctx? t

partial def Lean.Elab.InfoTree.findSomeM?.go {m : Type → Type} [Monad m] {α : Type} (f : ContextInfo → Info → PersistentArray InfoTree → m (Option α)) (ctx? : Option ContextInfo) : InfoTree → m (Option α)

Accumulates contexts and visits nodes if ctx? is not none.

def Lean.Elab.InfoTree.findSome? {α : Type} (f : ContextInfo → Info → PersistentArray InfoTree → Option α) (t : InfoTree) (ctx? : Option ContextInfo := none) : Option α

Finds the first result of f ctx info children which is some a, descending the tree from the top. Merges and updates contexts as it descends the tree.

f is only evaluated on nodes when some context is present. An initial context should be provided via the ctx? argument if invoking findSome? during a larger traversal of the infotree. A failure to provide ctx? := some ctx when t is not the outermost InfoTree is thus likely to cause findSome? to always return none.

Equations

• Lean.Elab.InfoTree.findSome? f t ctx? = (Lean.Elab.InfoTree.findSomeM? f t ctx?).run

def Lean.Elab.InfoTree.onHighestNode? {α : Type} (t : InfoTree) (ctx? : Option ContextInfo) (f : ContextInfo → Info → PersistentArray InfoTree → α) : Option α

Returns the value of f ctx info children on the outermost .node info children which has context, having merged and updated contexts appropriately.

If ctx? is some ctx, ctx is used as an initial context. A ctx? of none should only be used when operating on the first node of the entire infotree. Otherwise, it is likely that no context will be found.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.InfoTree.getDeclsByBody (t : InfoTree) : List Name

Get the parentDecls of every elaborated body.

This includes let rec/where definitions, but excludes decls without "bodies" (such as aliases, structures, declarations generated by attributes like @[ext], and so on) as we might find by considering every parentDeclCtx throughout the infotree.

Assumes that every body elaboration proceeds through Lean.Elab.Term.BodyInfo.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.InfoTree.getTheorems (t : InfoTree) (env : Environment) : List ConstantVal

Get the declarations elaborated in the infotree t which are theorems according to the environment. This includes e.g. instances of Prop classes in addition to declarations declared using the keyword theorem directly.

Equations

• t.getTheorems env = List.filterMap (fun (decl : Lean.Name) => env.findTheoremConstVal? decl) t.getDeclsByBody