Lean 语言参考手册

20.7. 字符🔗

字符由 Char 类型表示，它可以是任何 Unicode 标量值。 字符串是 UTF-8 编码的字节数组，而字符则由完整的 32 位值表示。 Lean 为字符字面量提供了特殊的语法。

20.7.1. 逻辑模型🔗

从 Lean 的逻辑角度来看，字符由一个 32 位无符号整数和一个证明它是有效 Unicode 标量值的证明组成。

🔗结构体
Char : Type
Char : Type

字符是 Unicode 标量值。

构造子

Char.mk

字段

val : UInt32

以 UInt32 表示的底层 Unicode 标量值。

valid : self.val.isValidChar

该值必须是合法的标量值。

20.7.2. 运行时表示🔗

作为一个平凡包装器，字符的表示方式与 UInt32 完全相同。 特别地，在单态语境中，字符被表示为 32 位立即数。 换句话说，类型为 Char 的构造子或结构体的字段不需要间接引用即可访问。 在多态语境中，字符是装箱的。

20.7.3. 语法🔗

字符字面量由包含在单引号（'，Unicode 'APOSTROPHE' (U+0027)）内的单个字符或转义序列组成。 在这些单引号之间，字符字面量可以包含除 ' 之外的字符，包括换行符，这些字符将被字面量地包含进来（无论文件编码和平台如何，Lean 源文件中的所有换行符都会被解释为 '\n'）。 特殊字符可以使用反斜杠进行转义，因此 '\'' 是一个包含单引号的字符字面量。 接受以下形式的转义序列：

\r, \n, \t, \\, \", \'

这些转义序列具有通常的含义，分别映射到 CR、LF、制表符、反斜杠、双引号和单引号。

\xNN

当 NN 是两个十六进制数字的序列时，此转义序列表示其 Unicode 代码点由该两位十六进制代码指定的字符。

\uNNNN

当 NN 是四个十六进制数字的序列时，此转义序列表示其 Unicode 代码点由该四位十六进制代码指定的字符。

20.7.4. API 参考🔗

20.7.4.1. 转换🔗

🔗定义
Char.ofNat (n : Nat) : Char
Char.ofNat (n : Nat) : Char

将 Nat 转换为 Char。如果 Nat 未编码有效的 Unicode 标量值，则返回 '\0'。

🔗定义
Char.toNat (c : Char) : Nat
Char.toNat (c : Char) : Nat

该字符的 Unicode 代码点为 Nat。

🔗定义
Char.isValidCharNat (n : Nat) : Prop
Char.isValidCharNat (n : Nat) : Prop

对于有效的 Unicode 标量 值 的自然数为 true。

🔗定义
Char.ofUInt8 (n : UInt8) : Char
Char.ofUInt8 (n : UInt8) : Char

将 8 位无符号整数转换为字符。

该整数的值被解释为 Unicode 代码点。

🔗定义
Char.toUInt8 (c : Char) : UInt8
Char.toUInt8 (c : Char) : UInt8

将字符转换为包含其代码点的 UInt8。

如果代码点大于 255，则会被截断（模 256 减少）。

有两种方法可以将字符转换为字符串。 Char.toString 将字符转换为仅包含该字符的单字符字符串，而 Char.quote 将字符转换为相应字符字面量的字符串表示。

🔗定义
Char.toString (c : Char) : String
Char.toString (c : Char) : String

构造一个仅包含所提供字符的单例字符串。

示例：

🔗定义
Char.quote (c : Char) : String
Char.quote (c : Char) : String

将字符引用为字符文字的表示形式，用单引号括起来并根据需要进行转义。

示例：

从字符到字符串

Char.toString 生成一个仅包含该字符的字符串：

"e"#eval 'e'.toString 
"e"
"e"#eval '\x65'.toString 
"e"
"\""#eval '"'.toString 
"\""

Char.quote 生成一个包含经过适当转义的字符字面量的字符串：

"'e'"#eval 'e'.quote 
"'e'"
"'e'"#eval '\x65'.quote 
"'e'"
"'\\\"'"#eval '"'.quote 
"'\\\"'"
在线查看 ↪

20.7.4.2. 字符类🔗

🔗定义
Char.isAlpha (c : Char) : Bool
Char.isAlpha (c : Char) : Bool

如果字符是 ASCII 字母，则返回 true。

ASCII 字母如下：ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz。

🔗定义
Char.isAlphanum (c : Char) : Bool
Char.isAlphanum (c : Char) : Bool

如果字符是 ASCII 字母或数字，则返回 true。

ASCII 字母如下：ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz。 ASCII 数字如下：0123456789。

🔗定义
Char.isDigit (c : Char) : Bool
Char.isDigit (c : Char) : Bool

如果字符是 ASCII 数字，则返回 true。

ASCII 数字如下：0123456789。

🔗定义
Char.isLower (c : Char) : Bool
Char.isLower (c : Char) : Bool

如果字符是小写 ASCII 字母，则返回 true。

小写 ASCII 字母如下：abcdefghijklmnopqrstuvwxyz。

🔗定义
Char.isUpper (c : Char) : Bool
Char.isUpper (c : Char) : Bool

如果字符是大写 ASCII 字母，则返回 true。

大写 ASCII 字母如下：ABCDEFGHIJKLMNOPQRSTUVWXYZ。

🔗定义
Char.isWhitespace (c : Char) : Bool
Char.isWhitespace (c : Char) : Bool

当字符为空格时返回 true；空格包括 (' ', U+0020)、制表符 ('\t', U+0009)、回车符 ('\r', U+000D) 或换行符 ('\n', U+000A)。

20.7.4.3. 大小写转换🔗

🔗定义
Char.toUpper (c : Char) : Char
Char.toUpper (c : Char) : Char

将小写 ASCII 字母转换为相应的大写字母。 ASCII 字母表之外的字母将原样返回。

小写 ASCII 字母如下：abcdefghijklmnopqrstuvwxyz。

🔗定义
Char.toLower (c : Char) : Char
Char.toLower (c : Char) : Char

将大写 ASCII 字母转换为相应的小写字母。 ASCII 字母表之外的字母将原样返回。

大写 ASCII 字母如下：ABCDEFGHIJKLMNOPQRSTUVWXYZ。

20.7.4.4. 比较🔗

🔗定义
Char.le (a b : Char) : Prop
Char.le (a b : Char) : Prop

如果一个字符的代码点小于或等于另一个字符的代码点，则该字符小于或等于另一个字符。

🔗定义
Char.lt (a b : Char) : Prop
Char.lt (a b : Char) : Prop

如果一个字符的代码点严格小于另一个字符的代码点，则该字符小于另一个字符。

20.7.4.5. Unicode🔗

🔗定义
Char.utf8Size (c : Char) : Nat
Char.utf8Size (c : Char) : Nat

返回以 UTF-8 编码此 Char 所需的字节数。