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.getHighestInfo? (t : InfoTree) (ctx? : Option ContextInfo) : Option (ContextInfo × Info)

Returns the context and info on the outermost .node info _ 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

• t.getHighestInfo? ctx? = t.onHighestNode? ctx? fun (ctx : Lean.Elab.ContextInfo) (i : Lean.Elab.Info) (x : Lean.PersistentArray Lean.Elab.InfoTree) => (ctx, i)

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.getDeclBodyInfos (t : InfoTree) : List (Syntax × ContextInfo × Info)

Gets the first child info of each Lean.Elab.BodyInfo, which should be the only child, and should be a TermInfo, PartialTermInfo, or TacticInfo. getDeclBodyInfos does not validate either of these conditions.

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

def Lean.Elab.Info.getLCtx? : Info → Option (LocalContext × Option Expr)

Gets the local context, and the expected type of the Info. Handles TacticInfos (looking at the first goal), TermInfos, and PartialTermInfos. Does not get the metavariable context; assumes that the caller has accumulated an ambient ContextInfo at this point which is sufficient.

Equations

• (Lean.Elab.Info.ofTacticInfo i).getLCtx? = do let g ← i.goalsBefore.head? let decl ← i.mctxBefore.findDecl? g some (decl.lctx, some decl.type)
• (Lean.Elab.Info.ofTermInfo i).getLCtx? = some (i.lctx, i.expectedType?)
• (Lean.Elab.Info.ofPartialTermInfo i).getLCtx? = some (i.lctx, i.expectedType?)
• x✝.getLCtx? = none