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. trees is visited in order and suggestions in each tree are collected in post-order.

Equations

• Lean.Elab.collectTryThisSuggestions trees = (StateT.run (Lean.Elab.collectTryThisSuggestions.go trees) #[]).snd

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

Visits all trees.

Equations

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

def Lean.Elab.collectTryThisSuggestions.visitNode (_ctx : ContextInfo) (i : Info) (_children : PersistentArray InfoTree) : StateM (Array Meta.Tactic.TryThis.Suggestion) Unit

Visits a node in a tree.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.collectTryThisSuggestions.visitNode _ctx i _children = pure PUnit.unit

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