@[reducible, inline]

abbrev Std.Sat.Literal (α : Type u) : Type u

CNF literals identified by some type α. The Bool is the polarity of the literal. true means positive polarity.

Equations

• Std.Sat.Literal α = (α × Bool)

def Std.Sat.Literal.negate {α : Type u_1} (l : Std.Sat.Literal α) : Std.Sat.Literal α

Flip the polarity of l.

Equations

• l.negate = (l.fst, !l.snd)