updateReducibility

Mathlib.Tactic.Linarith.Frontend

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.LinarithConfig.updateReducibility

Lean4

/-- `cfg.updateReducibility reduce_default` will change the transparency setting of `cfg` to
`default` if `reduce_default` is true. In this case, it also sets the discharger to `ring!`,
since this is typically needed when using stronger unification.
-/
def updateReducibility (cfg : LinarithConfig) (reduce_default : Bool) : LinarithConfig :=
  if reduce_default then
    { cfg with transparency := .default,
      discharger := do
        evalTactic (← `(tactic| ring1!)) }
  else cfg

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

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

Разделы

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

Аффилиация

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