inductive Lean.LBool : Type

• false: Lean.LBool
• true: Lean.LBool
• undef: Lean.LBool

instance Lean.instInhabitedLBool : Inhabited Lean.LBool

Equations

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

instance Lean.instBEqLBool : BEq Lean.LBool

def Lean.LBool.neg : Lean.LBool → Lean.LBool

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

def Lean.LBool.toString : Lean.LBool → String

instance Lean.LBool.instToString : ToString Lean.LBool

Equations

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

def Bool.toLBool : Bool → Lean.LBool

Equations

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

@[inline]

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

Equations

• toLBoolM x = do let b ← x pure b.toLBool