source
@[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)

Instances For

source
@[inline]
def Std.Sat.Literal.negate {α : Type u_1} (l : Literal α) :
Literal α

Flip the polarity of `l`.

Equations

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

Instances For