contains

Mathlib.Tactic.Linter.DirectoryDependency

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

Lean4

/-- Is a prefix of `n₁` related to a prefix of `n₂`? -/
def contains (r : NamePrefixRel) (n₁ n₂ : Name) : Bool :=
  (r.find n₁ n₂).isSome

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

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

Разделы

Аффилиация

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