structure Trestle.Literal (ν : Type u) : Type u

• toVar : ν
• polarity : Bool

instance Trestle.instReprLiteral {ν✝ : Type u_1} [Repr ν✝] : Repr (Literal ν✝)

Equations

• Trestle.instReprLiteral = { reprPrec := Trestle.reprLiteral✝ }

instance Trestle.instDecidableEqLiteral {ν✝ : Type u_1} [DecidableEq ν✝] : DecidableEq (Literal ν✝)

Equations

• Trestle.instDecidableEqLiteral = Trestle.decEqLiteral✝

instance Trestle.instInhabitedLiteral {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Literal a✝)

Equations

• Trestle.instInhabitedLiteral = { default := { toVar := default, polarity := default } }

instance Trestle.Literal.instLitVar {ν : Type u_1} : LitVar (Literal ν) ν

Equations

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

instance Trestle.Literal.instLawfulLitVar {ν : Type u_1} : LawfulLitVar (Literal ν) ν

@[reducible, inline]

abbrev Trestle.Literal.pos {ν : Type u_1} : ν → Literal ν

Equations

• Trestle.Literal.pos = Trestle.LitVar.mkPos

@[reducible, inline]

abbrev Trestle.Literal.neg {ν : Type u_1} : ν → Literal ν

Equations

• Trestle.Literal.neg = Trestle.LitVar.mkNeg