Lean 语言参考

20.7. 人物🔗

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

20.7.1. 逻辑模型🔗

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

🔗structure
Char : Type
Char : Type

Characters are Unicode scalar values.

Constructor

Char.mk

Fields

val : UInt32

The underlying Unicode scalar value as a UInt32.

valid : self.val.isValidChar

The value must be a legal scalar value.

20.7.2. 运行时表示🔗

作为 普通包装器，字符的表示方式与 UInt32 相同。 特别是，字符在单态上下文中表示为 32 位立即值。 换句话说，Char 类型的构造函数或结构体的字段不需要间接访问。 在多态上下文中，字符为 boxed。

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. 转换🔗

🔗def
Char.ofNat (n : Nat) : Char
Char.ofNat (n : Nat) : Char

Converts a Nat into a Char. If the Nat does not encode a valid Unicode scalar value, '\0' is returned instead.

🔗def
Char.toNat (c : Char) : Nat
Char.toNat (c : Char) : Nat

The character's Unicode code point as a Nat.

🔗def
Char.isValidCharNat (n : Nat) : Prop
Char.isValidCharNat (n : Nat) : Prop

True for natural numbers that are valid Unicode scalar values.

🔗def
Char.ofUInt8 (n : UInt8) : Char
Char.ofUInt8 (n : UInt8) : Char

Converts an 8-bit unsigned integer into a character.

The integer's value is interpreted as a Unicode code point.

🔗def
Char.toUInt8 (c : Char) : UInt8
Char.toUInt8 (c : Char) : UInt8

Converts a character into a UInt8 that contains its code point.

If the code point is larger than 255, it is truncated (reduced modulo 256).

将字符转换为字符串有两种方法。 Char.toString 将字符转换为仅包含该字符的单例字符串，而 Char.quote 将字符转换为相应字符文字的字符串表示形式。

🔗def
Char.toString (c : Char) : String
Char.toString (c : Char) : String

Constructs a singleton string that contains only the provided character.

Examples:

🔗def
Char.quote (c : Char) : String
Char.quote (c : Char) : String

Quotes the character to its representation as a character literal, surrounded by single quotes and escaped as necessary.

Examples:

From Characters to Strings

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 
"'\\\"'"
Live ↪

20.7.4.2. 字符类🔗

🔗def
Char.isAlpha (c : Char) : Bool
Char.isAlpha (c : Char) : Bool

Returns true if the character is an ASCII letter.

The ASCII letters are the following: ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz.

🔗def
Char.isAlphanum (c : Char) : Bool
Char.isAlphanum (c : Char) : Bool

Returns true if the character is an ASCII letter or digit.

The ASCII letters are the following: ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz. The ASCII digits are the following: 0123456789.

🔗def
Char.isDigit (c : Char) : Bool
Char.isDigit (c : Char) : Bool

Returns true if the character is an ASCII digit.

The ASCII digits are the following: 0123456789.

🔗def
Char.isLower (c : Char) : Bool
Char.isLower (c : Char) : Bool

Returns true if the character is a lowercase ASCII letter.

The lowercase ASCII letters are the following: abcdefghijklmnopqrstuvwxyz.

🔗def
Char.isUpper (c : Char) : Bool
Char.isUpper (c : Char) : Bool

Returns true if the character is a uppercase ASCII letter.

The uppercase ASCII letters are the following: ABCDEFGHIJKLMNOPQRSTUVWXYZ.

🔗def
Char.isWhitespace (c : Char) : Bool
Char.isWhitespace (c : Char) : Bool

Returns true if the character is a space (' ', U+0020), a tab ('\t', U+0009), a carriage return ('\r', U+000D), or a newline ('\n', U+000A).

20.7.4.3. 大小写转换🔗

🔗def
Char.toUpper (c : Char) : Char
Char.toUpper (c : Char) : Char

Converts a lowercase ASCII letter to the corresponding uppercase letter. Letters outside the ASCII alphabet are returned unchanged.

The lowercase ASCII letters are the following: abcdefghijklmnopqrstuvwxyz.

🔗def
Char.toLower (c : Char) : Char
Char.toLower (c : Char) : Char

Converts an uppercase ASCII letter to the corresponding lowercase letter. Letters outside the ASCII alphabet are returned unchanged.

The uppercase ASCII letters are the following: ABCDEFGHIJKLMNOPQRSTUVWXYZ.

20.7.4.4. 比较🔗

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

One character is less than or equal to another if its code point is less than or equal to the other's.

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

One character is less than another if its code point is strictly less than the other's.

20.7.4.5. Unicode🔗

🔗def
Char.utf8Size (c : Char) : Nat
Char.utf8Size (c : Char) : Nat

Returns the number of bytes required to encode this Char in UTF-8.

🔗def
Char.utf16Size (c : Char) : UInt32
Char.utf16Size (c : Char) : UInt32

Returns the number of bytes required to encode this Char in UTF-16.