Documentation

Init.Data.Char.Basic

@[inline]
noncomputable def isValidChar (n : UInt32) :
Prop
Equations
noncomputable def Char.lt (a : Char) (b : Char) :
Prop
Equations
noncomputable def Char.le (a : Char) (b : Char) :
Prop
Equations
instance Char.instLTChar :
Equations
instance Char.instLEChar :
Equations
@[inline]
abbrev Char.isValidCharNat (n : Nat) :
Prop
Equations
@[inline]
def Char.toNat (c : Char) :
Equations
def Char.isUpper (c : Char) :
Equations
def Char.isLower (c : Char) :
Equations
def Char.isDigit (c : Char) :
Equations
def Char.toLower (c : Char) :
Equations
def Char.toUpper (c : Char) :
Equations