distribNotAt

Mathlib.Tactic.Tauto

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Tauto.distribNotAt

Lean4

/-- Calls `distribNotAt` on the head of `state.fvars` up to `nIters` times, returning
early on failure.
-/
partial def distribNotAt (nIters : Nat) (state : DistribNotState) : MetaM DistribNotState :=
  match nIters, state.fvars with
  | 0, _ | _, [] => pure state
  | n + 1, fv :: fvs => do
    try
      let result ← distribNotOnceAt fv state.currentGoal
      let newFVars := mkFVar result.fvarId :: fvs.map (fun x ↦ result.subst.apply x)
      distribNotAt n ⟨newFVars, result.mvarId⟩
    catch _ =>
      pure state

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

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

Разделы

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

Аффилиация

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