Documentation

Lean.Data.LBool

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:

Equations

Lean.instBEqLBool = { beq := [anonymous] }

def Lean.LBool.neg:

Lean.LBool → Lean.LBool

Equations

Lean.LBool.neg _fun_discr = match _fun_discr with | Lean.LBool.true => Lean.LBool.false | Lean.LBool.false => Lean.LBool.true | Lean.LBool.undef => Lean.LBool.undef

def Lean.LBool.and:

Lean.LBool → Lean.LBool → Lean.LBool

Equations

Lean.LBool.and _fun_discr _fun_discr = match _fun_discr, _fun_discr with | Lean.LBool.true, b => b | a, x => a

def Lean.LBool.toString:

Lean.LBool → String

Equations

Lean.LBool.toString _fun_discr = match _fun_discr with | Lean.LBool.true => "true" | Lean.LBool.false => "false" | Lean.LBool.undef => "undef"

instance Lean.LBool.instToStringLBool:

ToString Lean.LBool

Equations

Lean.LBool.instToStringLBool = { toString := Lean.LBool.toString }

def Bool.toLBool:

Bool → Lean.LBool

Equations

Bool.toLBool _fun_discr = match _fun_discr with | true => Lean.LBool.true | false => Lean.LBool.false

@[inline]

def toLBoolM {m : Type → Type} [inst : Monad m] (x : m Bool) :

Equations

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