tacticBddDefault

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#tacticBddDefault

Lean4

/-- Sets are automatically bounded or cobounded in complete lattices. To use the same statements
in complete and conditionally complete lattices but let automation fill automatically the
boundedness proofs in complete lattices, we use the tactic `bddDefault` in the statements,
in the form `(hA : BddAbove A := by bddDefault)`. -/
@[tactic_parser 1000]
public meta def tacticBddDefault : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `tacticBddDefault 1024 (ParserDescr.nonReservedSymbol✝ "bddDefault" false✝)

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

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

Разделы

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

Аффилиация

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