prefixToName

Mathlib.Tactic.Linter.DirectoryDependency

URI: https://scilib.ai/kg/mathlib#Lean.Name.prefixToName

Lean4

/-- Find a name in `ns` that starts with prefix `p`. -/
def prefixToName (p : Name) (ns : Array Name) : Option Name :=
  ns.find? p.isPrefixOf

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

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

Разделы

Аффилиация

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