Documentation

Lean.Data.LBool

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