mkOrList

Mathlib.Tactic.MkIffOfInductiveProp

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

Lean4

/-- `mkOrList [x1, x2, ...]` is defined as `x1 ∨ (x2 ∨ ...)`, or `False` if the list is empty. -/
def mkOrList : List Expr → Expr :=
  mkOpList (mkConst `Or) (mkConst `False)

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

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

Разделы

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

Аффилиация

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