From 3aeb3db3b5915fecf116272fd8bca25d0e1a5d65 Mon Sep 17 00:00:00 2001
From: "E.W.Ayers" <edward.ayers@outlook.com>
Date: Fri, 26 Aug 2022 11:33:17 +0100
Subject: [PATCH] doc: Char/Basic.lean

---
 src/Init/Data/Char/Basic.lean | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean
index 918bae5688..970af62506 100644
--- a/src/Init/Data/Char/Basic.lean
+++ b/src/Init/Data/Char/Basic.lean
@@ -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