use_distrib

Mathlib.Tactic.Push

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Push.push_neg.use_distrib

Lean4

/-- Make `push_neg` use `not_and_or` rather than the default `not_and`. -/
@[init initFn✝, ]
opaque use_distrib : Lean.Option✝ Bool

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

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

Разделы

Аффилиация

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