inductive Lean.LBool : Type

• false : LBool
• true : LBool
• undef : LBool

@[instance_reducible]

instance Lean.instInhabitedLBool : Inhabited LBool

Equations

• Lean.instInhabitedLBool = { default := Lean.instInhabitedLBool.default }

@[instance_reducible]

instance Lean.instBEqLBool : BEq LBool

Equations

• Lean.instBEqLBool = { beq := Lean.instBEqLBool.beq }

def Lean.instBEqLBool.beq : LBool → LBool → Bool

Equations

• Lean.instBEqLBool.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Lean.LBool.neg : LBool → LBool

Equations

• Lean.LBool.true.neg = Lean.LBool.false
• Lean.LBool.false.neg = Lean.LBool.true
• Lean.LBool.undef.neg = Lean.LBool.undef

def Lean.LBool.and : LBool → LBool → LBool

Equations

• Lean.LBool.true.and x✝ = x✝
• x✝¹.and x✝ = x✝¹

def Lean.LBool.toString : LBool → String

Equations

• Lean.LBool.true.toString = "true"
• Lean.LBool.false.toString = "false"
• Lean.LBool.undef.toString = "undef"

@[instance_reducible]

instance Lean.LBool.instToString : ToString LBool

Equations

• Lean.LBool.instToString = { toString := Lean.LBool.toString }

def Lean.Bool.toLBool : Bool → LBool

Equations

• Lean.Bool.toLBool true = Lean.LBool.true
• Lean.Bool.toLBool false = Lean.LBool.false

@[inline]

def Lean.toLBoolM {m : Type → Type} [Monad m] (x : m Bool) : m LBool

Equations

• Lean.toLBoolM x = do let b ← x pure (Lean.Bool.toLBool b)