containsKey

Mathlib.Tactic.Linter.DirectoryDependency

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

Lean4

/-- Does `r` contain any entries with key `n`? -/
def containsKey (r : NamePrefixRel) (n : Name) : Bool :=
  NameMap.contains r n

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

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

Разделы

Аффилиация

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