declPriority

Mathlib.Tactic.Bound.Attribute

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Bound.declPriority

Lean4

/-- Map a theorem decl to a score (0 means `norm apply`, `0 <` means `safe apply`) -/
def declPriority (decl : Lean.Name) : Lean.MetaM Nat := do
  match (← Lean.getEnv).find? decl with
  | some info =>
    do
      typePriority decl info.type
  | none =>
    throwError "unknown declaration {decl}"

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

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

Разделы

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

Аффилиация

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