max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: Char/Basic.lean

Browse source
This commit is contained in:
E.W.Ayers 2022-08-26 11:33:17 +01:00 • committed by Leonardo de Moura
parent 5611620d3a
commit 3aeb3db3b5
1 changed files with 20 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Init/Data/Char/Basic.lean
View file

@ -6,6 +6,10 @@ Author: Leonardo de Moura
prelude
import Init.Data.UInt
/-- Determines if the given integer is a valid [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).
Note that values in `[0xd800, 0xdfff]` are reserved for [UTF-16 surrogate pairs](https://en.wikipedia.org/wiki/Universal_Character_Set_characters#Surrogates).
-/
@[inline, reducible] def isValidChar (n : UInt32) : Prop :=
n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)
@ -23,6 +27,7 @@ instance (a b : Char) : Decidable (a < b) :=
instance (a b : Char) : Decidable (a ≤ b) :=
UInt32.decLe _ _
/-- Determines if the given nat is a valid [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).-/
abbrev isValidCharNat (n : Nat) : Prop :=
n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)
@ -43,34 +48,49 @@ theorem isValidChar_of_isValidChar_Nat (n : Nat) (h : isValidCharNat n) : isVali
theorem isValidChar_zero : isValidChar 0 :=
Or.inl (by decide)
/-- Underlying unicode code point as a `Nat`. -/
@[inline] def toNat (c : Char) : Nat :=
c.val.toNat
instance : Inhabited Char where
default := 'A'
/-- Is the character a space (U+0020) a tab (U+0009), a carriage return (U+000D) or a newline (U+000A)? -/
def isWhitespace (c : Char) : Bool :=
c = ' ' || c = '\t' || c = '\r' || c = '\n'
/-- Is the character in `ABCDEFGHIJKLMNOPQRSTUVWXYZ`? -/
def isUpper (c : Char) : Bool :=
c.val ≥ 65 && c.val ≤ 90
/-- Is the character in `abcdefghijklmnopqrstuvwxyz`? -/
def isLower (c : Char) : Bool :=
c.val ≥ 97 && c.val ≤ 122
/-- Is the character in `ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz`? -/
def isAlpha (c : Char) : Bool :=
c.isUpper || c.isLower
/-- Is the character in `0123456789`? -/
def isDigit (c : Char) : Bool :=
c.val ≥ 48 && c.val ≤ 57
/-- Is the character in `ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789`? -/
def isAlphanum (c : Char) : Bool :=
c.isAlpha || c.isDigit
/-- Convert an upper case character to its lower case character.
Only works on basic latin letters.
-/
def toLower (c : Char) : Char :=
let n := toNat c;
if n >= 65 ∧ n <= 90 then ofNat (n + 32) else c
/-- Convert a lower case character to its upper case character.
Only works on basic latin letters.
-/
def toUpper (c : Char) : Char :=
let n := toNat c;
if n >= 97 ∧ n <= 122 then ofNat (n - 32) else c