mkAndList

Mathlib.Tactic.MkIffOfInductiveProp

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

Lean4

/-- `mkAndList [x1, x2, ...]` is defined as `x1 ∧ (x2 ∧ ...)`, or `True` if the list is empty. -/
def mkAndList : List Expr → Expr :=
  mkOpList (mkConst `And) (mkConst `True)

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

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

Разделы

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

Аффилиация

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