Literals

@[specialize #[]]

class Trestle.LitVar (L : Type u) (ν : outParam (Type v)) : Type (max u v)

The type L is a representation of literals over variables of type ν.

• negate : L → L
• mkPos : ν → L
• mkNeg : ν → L
• toVar : L → ν
• polarity : L → Bool

  true if positive

def Trestle.LitVar.mkLit (L : Type u) {ν : Type v} [LitVar L ν] (x : ν) (p : Bool) : L

Equations

• Trestle.LitVar.mkLit L x p = if p = true then Trestle.LitVar.mkPos x else Trestle.LitVar.mkNeg x

def Trestle.LitVar.map {L : Type u_1} {V : Type u_2} {L' : Type u_3} {V' : Type u_4} [LitVar L V] [LitVar L' V'] (f : V → V') (l : L) : L'

Equations

• Trestle.LitVar.map f l = Trestle.LitVar.mkLit L' (f (Trestle.LitVar.toVar l)) (Trestle.LitVar.polarity l)

instance Trestle.LitVar.instCoe {L : Type u} {ν : Type v} [LitVar L ν] : Coe ν L

Equations

• Trestle.LitVar.instCoe = { coe := Trestle.LitVar.mkPos }

instance Trestle.LitVar.instNeg {L : Type u} {ν : Type v} [LitVar L ν] : Neg L

Equations

• Trestle.LitVar.instNeg = { neg := Trestle.LitVar.negate }

@[simp]

theorem Trestle.LitVar.negate_eq {L : Type u} {ν : Type v} [LitVar L ν] (l : L) : negate l = -l

instance Trestle.LitVar.instToString {L : Type u} {ν : Type v} [LitVar L ν] [ToString ν] : ToString L

Equations

• One or more equations did not get rendered due to their size.

Lawful literals

class Trestle.LawfulLitVar (L : Type u) (ν : outParam (Type v)) [LitVar L ν] : Prop

• toVar_negate (l : L) : LitVar.toVar (-l) = LitVar.toVar l
• toVar_mkPos (x : ν) : LitVar.toVar (LitVar.mkPos x) = x
• toVar_mkNeg (x : ν) : LitVar.toVar (LitVar.mkNeg x) = x
• polarity_negate (l : L) : LitVar.polarity (-l) = !LitVar.polarity l
• polarity_mkPos (x : ν) : LitVar.polarity (LitVar.mkPos x) = true
• polarity_mkNeg (x : ν) : LitVar.polarity (LitVar.mkNeg x) = false
• ext (l₁ l₂ : L) : LitVar.toVar l₁ = LitVar.toVar l₂ → LitVar.polarity l₁ = LitVar.polarity l₂ → l₁ = l₂

theorem Trestle.LawfulLitVar.ext_iff {L : Type u} {ν : outParam (Type v)} {inst✝ : LitVar L ν} [self : LawfulLitVar L ν] {l₁ l₂ : L} : l₁ = l₂ ↔ LitVar.toVar l₁ = LitVar.toVar l₂ ∧ LitVar.polarity l₁ = LitVar.polarity l₂

Sums as valid literals

instance Trestle.LitVar.instSum {L1 : Type u_1} {V1 : Type u_2} {L2 : Type u_3} {V2 : Type u_4} [LitVar L1 V1] [LitVar L2 V2] : LitVar (L1 ⊕ L2) (V1 ⊕ V2)

Equations

• One or more equations did not get rendered due to their size.