mkExistsList

Mathlib.Tactic.MkIffOfInductiveProp

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.MkIff.mkExistsList

Lean4

/-- Generates an expression of the form `∃ (args), inner`. `args` is assumed to be a list of fvars.
When possible, `p ∧ q` is used instead of `∃ (_ : p), q`. -/
def mkExistsList (args : List Expr) (inner : Expr) : MetaM Expr :=
  args.foldrM
    (fun arg i : Expr => do
      let t ← inferType arg
      let l := (← inferType t).sortLevel!
      if arg.occurs i || l != Level.zero then
        pure (mkApp2 (.const `Exists [l]) t (updateLambdaBinderInfoD! <| ← mkLambdaFVars #[arg] i))
      else
        pure <| mkApp2 (mkConst `And) t i)
    inner

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

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

Разделы

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

Аффилиация

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