intros!

Mathlib.Lean.Meta

URI: https://scilib.ai/kg/mathlib#Lean.MVarId.intros!

Lean4

/-- Applies `intro` repeatedly until it fails. We use this instead of
`Lean.MVarId.intros` to allowing unfolding.
For example, if we want to do introductions for propositions like `¬p`,
the `¬` needs to be unfolded into `→ False`, and `intros` does not do such unfolding. -/
partial def intros! (mvarId : MVarId) : MetaM (Array FVarId × MVarId) :=
  run #[] mvarId
where/-- Implementation of `intros!`. -/
   run (acc : Array FVarId) (g : MVarId) :=
    try
      let ⟨f, g⟩ ← mvarId.intro1
      run (acc.push f) g
    catch _ =>
      pure (acc, g)

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

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

Разделы

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

Аффилиация

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