Documentation

Std.Sat.CNF.Literal

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
    Instances For
      source
      @[inline]
      def Std.Sat.Literal.negate {α : Type u_1} (l : Literal α) :
      Literal α

      Flip the polarity of l.

      Equations
        Instances For