Documentation

Init.Data.Char.Basic

@[inline]

def isValidChar (n : UInt32) :

Prop

Equations

isValidChar n = (n < 55296 ∨ 57343 < n ∧ n < 1114112)

def Char.lt (a : Char) (b : Char) :

Prop

Equations

Char.lt a b = (a.val < b.val)

def Char.le (a : Char) (b : Char) :

Prop

Equations

Char.le a b = (a.val ≤ b.val)

instance Char.instLTChar:

Equations

Char.instLTChar = { lt := Char.lt }

instance Char.instLEChar:

Equations

Char.instLEChar = { le := Char.le }

instance Char.instDecidableLtCharInstLTChar (a : Char) (b : Char) :

Decidable (a < b)

Equations

Char.instDecidableLtCharInstLTChar a b = UInt32.decLt a.val b.val

instance Char.instDecidableLeCharInstLEChar (a : Char) (b : Char) :

Decidable (a ≤ b)

Equations

Char.instDecidableLeCharInstLEChar a b = UInt32.decLe a.val b.val

@[inline]

abbrev Char.isValidCharNat (n : Nat) :

Prop

Equations

Char.isValidCharNat n = (n < 55296 ∨ 57343 < n ∧ n < 1114112)

theorem Char.isValidUInt32 (n : Nat) (h : Char.isValidCharNat n) :

n < UInt32.size

theorem Char.isValidChar_of_isValidChar_Nat (n : Nat) (h : Char.isValidCharNat n) :

isValidChar (UInt32.ofNat' n (_ : n < UInt32.size))

theorem Char.isValidChar_zero:

@[inline]

def Char.toNat (c : Char) :

Equations

Char.toNat c = UInt32.toNat c.val

instance Char.instInhabitedChar:

Equations

Char.instInhabitedChar = { default := Char.ofNat 65 }

def Char.isWhitespace (c : Char) :

Equations

Char.isWhitespace c = (decide (c = Char.ofNat 32) || decide (c = Char.ofNat 9) || decide (c = Char.ofNat 13) || decide (c = Char.ofNat 10))

def Char.isUpper (c : Char) :

Equations

Char.isUpper c = (decide (c.val ≥ 65) && decide (c.val ≤ 90))

def Char.isLower (c : Char) :

Equations

Char.isLower c = (decide (c.val ≥ 97) && decide (c.val ≤ 122))

def Char.isAlpha (c : Char) :

Equations

Char.isAlpha c = (Char.isUpper c || Char.isLower c)

def Char.isDigit (c : Char) :

Equations

Char.isDigit c = (decide (c.val ≥ 48) && decide (c.val ≤ 57))

def Char.isAlphanum (c : Char) :

Equations

Char.isAlphanum c = (Char.isAlpha c || Char.isDigit c)

def Char.toLower (c : Char) :

Equations

Char.toLower c = let n := Char.toNat c; if n ≥ 65 ∧ n ≤ 90 then Char.ofNat (n + 32) else c

def Char.toUpper (c : Char) :

Equations

Char.toUpper c = let n := Char.toNat c; if n ≥ 97 ∧ n ≤ 122 then Char.ofNat (n - 32) else c