getAllLeft

Mathlib.Tactic.Linter.DirectoryDependency

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.DirectoryDependency.NamePrefixRel.getAllLeft

Lean4

/-- Look up all names `m` which are values of some prefix of `n` under this relation. -/
def getAllLeft (r : NamePrefixRel) (n : Name) : NameSet :=
  Id.run do
    let matchingPrefixes := n.prefixes.filter (fun prf ↦ r.containsKey prf)
    let mut allRules := NameSet.empty
    for prefix_ in matchingPrefixes do
      let some rules := r.find? prefix_ |
        unreachable!
      allRules := allRules.append rules
    allRules

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

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

Разделы

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

Аффилиация

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