Documentation

Std.Sat.CNF.Literal

@[reducible, inline]
abbrev Std.Sat.Literal (α : Type u) :

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

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

      Flip the polarity of l.

      Equations
        Instances For