getGoalLocations

Mathlib.Tactic.Widget.SelectPanelUtils

URI: https://scilib.ai/kg/mathlib#getGoalLocations

Lean4

/-- Given a `Array GoalsLocation` return the array of `SubExpr.Pos` for all locations
in the targets of the relevant goals. -/
def getGoalLocations (locations : Array GoalsLocation) : Array SubExpr.Pos :=
  Id.run
    (do
      let mut res := #[]
      for location in locations do
        if let .target pos := location.loc then
          res := res.push pos
      return res)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru