scoreToConfig

Mathlib.Tactic.Bound.Attribute

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

Lean4

/-- Map a score to either `norm apply` or `safe apply <priority>` -/
def scoreToConfig (decl : Lean.Name) (score : Nat) : Aesop.Frontend.RuleConfig :=
  let (phase, priority) :=
    match score with
    | 0 =>
      (Aesop.PhaseName.norm, 0) -- No hypotheses: this rule closes the goal immediately

    | s => (Aesop.PhaseName.safe, s)
  { term? := some (Lean.mkIdent decl)
    phase? := phase
    priority? := some (Aesop.Frontend.Priority.int priority)
    builder? := some (.regular .apply)
    builderOptions := { }
    ruleSets := ⟨#[`Bound]⟩ }

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

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

Разделы

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

Аффилиация

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