neg

Mathlib.Tactic.Sat.FromLRAT

URI: https://scilib.ai/kg/mathlib#Sat.Valuation.neg

Lean4

/-- `v.neg lit` asserts that literal `lit` is falsified in the valuation. -/
def neg (v : Valuation) : Literal → Prop
  | Literal.pos i => ¬v i
  | Literal.neg i => v i

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

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

Разделы

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

Аффилиация

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