@[inline]
Equations
- Char.instDecidableLtCharInstLTChar a b = UInt32.decLt a.val b.val
Equations
- Char.instDecidableLeCharInstLEChar a b = UInt32.decLe a.val b.val
@[inline]
theorem
Char.isValidChar_of_isValidChar_Nat
(n : Nat)
(h : Char.isValidCharNat n)
:
isValidChar (UInt32.ofNat' n (_ : n < UInt32.size))
Equations
- Char.instInhabitedChar = { default := Char.ofNat 65 }
Equations
- Char.isWhitespace c = (decide (c = Char.ofNat 32) || decide (c = Char.ofNat 9) || decide (c = Char.ofNat 13) || decide (c = Char.ofNat 10))
Equations
- Char.isAlpha c = (Char.isUpper c || Char.isLower c)
Equations
- Char.isAlphanum c = (Char.isAlpha c || Char.isDigit c)
Equations
- Char.toLower c = let n := Char.toNat c; if n ≥ 65 ∧ n ≤ 90 then Char.ofNat (n + 32) else c
Equations
- Char.toUpper c = let n := Char.toNat c; if n ≥ 97 ∧ n ≤ 122 then Char.ofNat (n - 32) else c