source
inductive Lean.LBool :
Type

- false : LBool
- true : LBool
- undef : LBool

Instances For

source
def Lean.instInhabitedLBool.default :
LBool
Equations

- Lean.instInhabitedLBool.default = Lean.LBool.false

Instances For

source
instance Lean.instInhabitedLBool :
Inhabited LBool
Equations

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

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

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

Instances For

source
instance Lean.instBEqLBool :
BEq LBool
Equations

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

source
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

Instances For

source
def Lean.LBool.and :
LBool → LBool → LBool
Equations

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

Instances For

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

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

Instances For

source
instance Lean.LBool.instToString :
ToString LBool
Equations

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

source
def Bool.toLBool :
Bool → Lean.LBool
Equations

- true.toLBool = Lean.LBool.true
- false.toLBool = Lean.LBool.false

Instances For

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

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

Instances For