字符串表示 Unicode 文本。 Lean 对字符串有特殊支持：
它们具有逻辑模型，该模型通过包含 UTF-8 标量值的 ByteArray 来指定其行为。
在编译后的代码中，它们有一个运行时表示，该表示额外包含了一个缓存的长度，以标量值的数量来衡量。 Lean 运行时提供了字符串操作的优化实现。
存在用于编写字符串的字符串字面量语法。
UTF-8 是一种可变宽度编码。 一个字符可以编码为一个、两个、三个或四个字节的代码单元。 字符串是 UTF-8 编码的字节数组这一事实在 API 中是可见的：
字符串由 String.Pos 索引，其在内部记录的是字节数而不是字符数，因此需要常量时间。
String.Pos 包含一个证明，证明字节计数实际上指向一个 UTF-8 代码单元的起始位置。
除了 0 之外，这些不应该直接构造，而应该使用 String.next 和 String.prev 来更新。
字符串是 Unicode 标量值的序列。
在运行时，字符串由使用 UTF-8 编码的字节的动态数组 表示。以字节为单位的大小 (String.utf8ByteSize) 和以字符为单位的大小 (String.length) 都会被缓存并占用恒定时间。当对字符串的引用是唯一的时，对字符串的许多操作都会执行就地修改。
字段
toByteArray : ByteArray
字符串 UTF-8 编码的字节。由于字符串在运行时采用特殊表示，此函数在运行时实际需要线性时间和空间。若要高效访问字符串的字节，请使用 String.utf8ByteSize 和 String.getUTF8Byte。
isValidUTF8 : self.toByteArray.IsValidUTF8
字符串的字节构成有效的 UTF-8。
Lean 中字符串的逻辑模型是一个包含两个字段的结构体：
String.toByteArray 是一个 ByteArray，包含了该字符串的 UTF-8 编码。
String.isValidUTF8 是一个证明，证明这些字节实际上是字符串的有效 UTF-8 编码。
此模型允许使用针对字节数组的操作在低级别上指定并证明关于字符串操作的属性，同时仍能建立在字节数组理论之上。 同时，它足够接近真实的运行时表示，从而避免了逻辑模型与运行时表示中有意义的操作之间的阻抗失配。
在 Lean 的早期版本中，字符串的逻辑模型是包含字符列表的结构体。
该模型仍然有用。
它仍然可以使用 String.ofList（将字符列表转换为 String）以及 String.toList（将 String 转换为字符列表）来访问。
创建一个字符串，其中按顺序包含列表中的字符。
示例：
String.ofList ['L', '∃', '∀', 'N'] = "L∃∀N"
String.ofList [] = ""
String.ofList ['a', 'a', 'a'] = "aaa"
字符串被表示为 UTF-8 编码的字节动态数组。 在对象头部之后，一个字符串包含：
当前包含有效字符串数据的字节数。
目前为该字符串分配的字节数。
编码后字符串的长度，由于 UTF-8 的多字节字符，它可能短于字节数。
字符串中实际的字符数据，以 null 结尾。
Lean 运行时中的许多字符串函数会通过查询对象头部中的引用计数，检查它们是否独占其参数。 如果是这样，并且字符串的容量足够，那么现有的字符串就可以被修改，而不是分配新的内存。 否则，必须分配一个新的字符串。
尽管它们看起来像是普通的构造子和投影，但 String.ofByteArray 和 String.toByteArray 需要的时间与字符串的长度成正比。
这是因为字节数组和字符串没有相同的表示，因此必须将字节数组的内容复制到一个新对象中。
Lean 有三类字符串字面量：普通字符串字面量、插值字符串字面量和原始字符串字面量。
字符串字面量以双引号字符 " 开始并结束。
在这两个字符之间，可以包含任意其他字符，包括换行；这些字符都会按字面纳入字符串（但要注意，不论文件编码和平台如何，Lean 源文件中的所有换行都会被解释为 '\n'）。
无法直接写入字符串字面量的特殊字符可以用反斜杠转义，因此 "\"Quotes\"" 是一个以双引号开头并以双引号结尾的字符串字面量。
可接受的转义序列形式如下：
\r, \n, \t, \\, \", \'
这些转义序列具有通常的含义，分别对应 CR、LF、制表符、反斜杠、双引号和单引号。
\xNN
当 NN 是由两个十六进制数字组成的序列时，该转义表示 Unicode 码点由这两个十六进制数字给出的字符。
\uNNNN
当 NN 是由四个十六进制数字组成的序列时，该转义表示 Unicode 码点由这四个十六进制数字给出的字符。
字符串字面量可以包含 间隙。 间隙由一个被转义的换行表示，也就是转义用的反斜杠与换行之间不能有其他字符。 在这种情况下，字面量所表示的字符串会省去该换行以及下一行开头的全部空白。 字符串间隙后面不能跟只含空白字符的行。
这里，str1 与 str2 是同一个字符串：
def str1 := "String with \
a gap"
def str2 := "String with a gap"
example : str1 = str2 := rfl
如果间隙后紧跟的那一行为空，则该字符串会被拒绝：
def str3 := "String with \a gap"
解析器错误为：
在字符串字面量前加上 s!，会使其被处理为 插值字符串：字符串中由 { 与 } 包围的部分会被解析并解释为 Lean 表达式。
插值字符串会被解释为：将插值前的字符串、该表达式（外围额外加上一层 toString 调用）以及插值后的字符串依次拼接。
例如：
example :
s!"1 + 1 = {1 + 1}\n" =
"1 + 1 = " ++ toString (1 + 1) ++ "\n" :=
rfl
在字面量前加上 m!，会使插值结果成为 MessageData 的一个实例；这是编译器内部用于向用户显示消息的数据结构。
在 原始字符串字面量 中， 没有转义序列，也没有间隙，每个字符都严格按其自身含义解释。
原始字符串字面量以 r 开头，后跟零个或多个井号字符（#）以及一个双引号 "。
当遇到一个后面紧跟着相同数量井号字符的双引号时，该字符串字面量结束。
例如，它们可用于避免某些字符需要双重转义：
example : r"\t" = "\\t" := rfl
#eval r"Write backslash in a string using '\\\\'"
该 #eval 的结果为：
加入井号后，字符串中就可以包含无需转义的引号：
example :
r#"This is "literally" quoted"# =
"This is \"literally\" quoted" :=
rfl
只要添加足够多的井号，任何原始字面量都可以被按字面写出：
example :
r##"This is r#"literally"# quoted"## =
"This is r#\"literally\"# quoted" :=
rfl
返回只含字符 c 的新字符串。
此段说明该操作的行为、边界条件及推荐用法。
以下列出相应示例或例外情况。
示例见所列代码。（相关项：String.singleton 'L' = "L"。）
示例见所列代码。（相关项：String.singleton ' ' = " "。）
示例见所列代码。（相关项：String.singleton '"' = "\""。）
示例见所列代码。（相关项：String.singleton '𝒫' = "𝒫"。）
连接两个字符串，通常通过运算符 ++ 使用。
若相关字符串未被共享，实现会尽可能进行原地更新而不复制。
以下列出相应示例或例外情况。
示例见所列代码。（相关项："abc".append "def" = "abcdef"。）
示例见所列代码。（相关项："abc" ++ "def" = "abcdef"。）
示例见所列代码。（相关项："" ++ "" = ""。）
按顺序连接一个字符串列表中的所有字符串。
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：String.intercalate。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项：String.join ["gr", "ee", "n"] = "green"。）
示例见所列代码。（相关项：String.join ["b", "", "l", "", "ue"] = "blue"。）
示例见所列代码。（相关项：String.join [] = ""。）
连接字符串列表中的字符串，并在每一对相邻字符串之间放置分隔符 s。
以下列出相应示例或例外情况。
示例见所列代码。（相关项：", ".intercalate ["red", "green", "blue"] = "red, green, blue"。）
示例见所列代码。（相关项：" and ".intercalate ["tea", "coffee"] = "tea and coffee"。）
示例见所列代码。（相关项：" | ".intercalate ["M", "", "N"] = "M | | N"。）
把字符串转换为字符列表。
字符串使用 UTF-8 编码；此操作的时间与空间特性如所述。
以下列出相应示例或例外情况。
示例见所列代码。（相关项："abc".toList = ['a', 'b', 'c']。）
示例见所列代码。（相关项："".toList = []。）
示例见所列代码。（相关项："\n".toList = ['\n']。）
检查字符串能否解释为自然数的十进制表示。
此段说明该操作的行为、边界条件及推荐用法。
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：toNat?、toNat!。）
示例：
检查字符串能否解释为整数的十进制表示。
此段说明该操作的行为、边界条件及推荐用法。（相关项：-、+。）
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：String.toInt?、String.toInt!。）
示例：
把字符串解释为整数的十进制表示并返回该数；若不是十进制整数则返回 none。
此段说明该操作的行为、边界条件及推荐用法。（相关项：-、+。）
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：String.isInt、String.toInt?、some、String.toInt!、none。）
示例：
把字符串解释为整数的十进制表示并返回该数；若不是十进制整数则触发 panic。
此段说明该操作的行为、边界条件及推荐用法。（相关项：-、+。）
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：String.isInt、String.toInt!、String.toInt?、none。）
示例：
Pos s 是 s 中的字节偏移，并带有该位置位于 UTF-8 字符边界上的证明。
构造子
String.Pos.mk
字段
offset : String.Pos.Raw
Pos 的底层字节偏移。
isValid : String.Pos.Raw.IsValid s self.offset
证明 offset 对字符串 s 有效。
根据一个位置及其有效性证明，构造 s 上的有效位置。
根据一个位置构造 s 上的有效位置；若该位置无效则触发 panic。
把字符串的一段区域复制到新字符串中。
此段说明该操作的行为、边界条件及推荐用法。（相关项：s、b、e、String。）
在所述条件下，函数按说明返回相应结果或后备结果。（相关项：b、e、""。）
在所述条件下，函数按说明返回相应结果或后备结果。（相关项：String.slice。）
返回字符串位置 pos 处的字符；若该位置是越尾位置则触发 panic。
运行时代码会用高效实现覆盖此函数。
用 p 作用于该字符所得的结果，替换字符串 s 中位置 f 处的字符。
若相关字符串未被共享，实现会尽可能进行原地更新而不复制。
以下列出相应示例或例外情况。
示例见所列代码。（相关项：("abc".pos ⟨1⟩ (by decide)).modify Char.toUpper (by decide) = "aBc"。）
返回字符串位置 pos 处的字节。
返回给定位置之前的有效位置；所给证明保证当前位置不是起始位置，因此前一位置存在。
返回给定位置之前的有效位置；若当前位置是起始位置则触发 panic。
把字符串上的有效位置推进到下一个有效位置；所给证明保证当前位置不是越尾位置，因此下一位置存在。
把字符串上的有效位置推进到下一个有效位置；若当前位置是越尾位置则触发 panic。
给定 t 的证明，把 s 上的有效位置转换为 s = t 上的有效位置。
给定字符串中的有效位置，在该位置位于被修改位置之前时，取得设置字符后字符串中的对应位置。
按照 UTF-8 编码表示 String 中字节位置的类型。
此段说明该操作的行为、边界条件及推荐用法。（相关项：Nat、String、String.Pos.Raw。）
位置或迭代器仅在满足所述边界与 UTF-8 字符边界条件时有效；无效输入的结果按说明处理。（相关项：p、s、0 ≤ p ≤ s.rawEndPos、p、String.Pos.IsValid。）
此段说明该操作的行为、边界条件及推荐用法。（相关项：String.Pos、String.Pos、String.Pos.Raw。）
字段
byteIdx : Nat
取得 String.Pos.Raw 的底层字节索引。
返回字符串中给定位置（即 UTF-8 字节索引）对应的字符索引。
在所述条件下，函数按说明返回相应结果或后备结果。
以下列出相应示例或例外情况。
示例见所列代码。（相关项："L∃∀N".offsetOfPos ⟨0⟩ = 0。）
示例见所列代码。（相关项："L∃∀N".offsetOfPos ⟨1⟩ = 1。）
示例见所列代码。（相关项："L∃∀N".offsetOfPos ⟨2⟩ = 2。）
示例见所列代码。（相关项："L∃∀N".offsetOfPos ⟨4⟩ = 2。）
示例见所列代码。（相关项："L∃∀N".offsetOfPos ⟨5⟩ = 3。）
示例见所列代码。（相关项："L∃∀N".offsetOfPos ⟨50⟩ = 4。）
若 true 是字符串 p 中有效的 UTF-8 位置，则返回 s。
字符串使用 UTF-8 编码；此操作的时间与空间特性如所述。（相关项：p ≤ s.rawEndPos、p。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项：String.Pos.isValid "abc" ⟨0⟩ = true。）
示例见所列代码。（相关项：String.Pos.isValid "abc" ⟨1⟩ = true。）
示例见所列代码。（相关项：String.Pos.isValid "abc" ⟨3⟩ = true。）
示例见所列代码。（相关项：String.Pos.isValid "abc" ⟨4⟩ = false。）
示例见所列代码。（相关项：String.Pos.isValid "𝒫(A)" ⟨0⟩ = true。）
示例见所列代码。（相关项：String.Pos.isValid "𝒫(A)" ⟨1⟩ = false。）
示例见所列代码。（相关项：String.Pos.isValid "𝒫(A)" ⟨2⟩ = false。）
示例见所列代码。（相关项：String.Pos.isValid "𝒫(A)" ⟨3⟩ = false。）
示例见所列代码。（相关项：String.Pos.isValid "𝒫(A)" ⟨4⟩ = true。）
高效检查某位置是否位于切片 s 的 UTF-8 字符边界上。
若指定字节位置大于或等于字符串越尾位置则返回 true，否则返回 false。
以下列出相应示例或例外情况。
示例见所列代码。（相关项：(0 |> "abc".next |> "abc".next |> "abc".atEnd) = false。）
示例见所列代码。（相关项：(0 |> "abc".next |> "abc".next |> "abc".next |> "abc".next |> "abc".atEnd) = true。）
示例见所列代码。（相关项：(0 |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".atEnd) = false。）
示例见所列代码。（相关项：(0 |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".atEnd) = true。）
示例见所列代码。（相关项："abc".atEnd ⟨4⟩ = true。）
示例见所列代码。（相关项："L∃∀N".atEnd ⟨7⟩ = false。）
示例见所列代码。（相关项："L∃∀N".atEnd ⟨8⟩ = true。）
返回 p₁ 与 p₂ 中字节索引较小的一个。
返回位置 lo 与 hi 所界定字节切片的大小。
String.Pos.Raw.substrEq (s1 : String) (pos1 : String.Pos.Raw) (s2 : String) (pos2 : String.Pos.Raw) (sz : Nat) : BoolString.Pos.Raw.substrEq (s1 : String) (pos1 : String.Pos.Raw) (s2 : String) (pos2 : String.Pos.Raw) (sz : Nat) : Bool
检查两个字符串的子串是否相等；子串由起始位置及其 UTF-8 字节数指定，任一子串不存在时返回 false。
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：BEq、String.Slice。）
返回字符串中指定位置 p 之前的位置。（相关项：p = ⟨0⟩、0、p、rawEndPos、p、p。）
此段说明该操作的行为、边界条件及推荐用法。（相关项："L∃∀N".prev ⟨3⟩、⟨1⟩、'∃'。）
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.Pos.prev、String.Pos.prev?、String.pos、String.Pos。）
以下列出相应示例或例外情况。
返回字符串中位置 p 之后的下一个位置。（相关项：p、p = s.endPos、p。）
此段说明该操作的行为、边界条件及推荐用法。（相关项：p、String.next'。）
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.Pos.next、String.Pos.next?、String.pos、String.ValisPos。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项："abc".next ⟨3⟩ = ⟨4⟩、3 = "abc".endPos。）
示例见所列代码。（相关项："L∃∀N".next ⟨2⟩ = ⟨3⟩、2。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项："abc".get ("abc".next 0) = 'b'。）
示例见所列代码。（相关项："L∃∀N".get (0 |> "L∃∀N".next |> "L∃∀N".next) = '∀'。）
String.Pos.Raw.next' (s : String) (p : String.Pos.Raw) (h : ¬String.Pos.Raw.atEnd s p = true) : String.Pos.RawString.Pos.Raw.next' (s : String) (p : String.Pos.Raw) (h : ¬String.Pos.Raw.atEnd s p = true) : String.Pos.Raw
返回字符串中位置 p 之后的下一个位置；若 p 无效，结果未指定。
此段说明该操作的行为、边界条件及推荐用法。（相关项：h、p、String.next。）
def next? (s : String) (p : String.Pos) : Option Char := if h : s.atEnd p then none else s.get (s.next' p h)
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.next'、if、String.Pos.next。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项：String.pos。）（相关项：String.Pos、let abc := "abc"; abc.get (abc.next' 0 (by decide)) = 'b'。）
像 String.Pos.Raw.next 一样反复推进位置，同时谓词 p 对当前位置字符返回 false；到达末尾或谓词返回 p 时停止。（相关项：true。）
示例：
示例见所列代码。（相关项：let s := " a "; (Pos.Raw.nextUntil s Char.isWhitespace 0).get s = ' '。）
示例见所列代码。（相关项：let s := " a "; (Pos.Raw.nextUntil s Char.isAlpha 0).get s = 'a'。）
示例见所列代码。（相关项：let s := "a "; (Pos.Raw.nextUntil s Char.isWhitespace 0).get s = ' '。）
像 String.Pos.Raw.next 一样反复推进位置，同时谓词 p 对当前位置字符返回 true；到达末尾或谓词返回 p 时停止。（相关项：false。）
示例：
示例见所列代码。（相关项：let s := " a "; ((0 : Pos.Raw).nextWhile s Char.isWhitespace).get s = 'a'。）
示例见所列代码。（相关项：let s := "a "; ((0 : Pos.Raw).nextWhile s Char.isWhitespace).get s = 'a'。）
示例见所列代码。（相关项：let s := "ba "; (Pos.Raw.nextWhile s Char.isWhitespace 0).get s = 'b'。）
把位置的字节偏移增加 1；不要与 Pos.next 混淆。
把 p 向前推进 n 个字节。（相关项：HAdd、c、s、p、p + c、p + s。）
此段说明该操作的行为、边界条件及推荐用法。
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：Pos.Raw.offsetBy。）
在左侧用 p 偏移 offset。（相关项：HAdd、c、s、c + p、s + p。）
此段说明该操作的行为、边界条件及推荐用法。
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：Pos.Raw.increaseBy。）
把位置的字节偏移减少 1；不要与 Pos.prev 混淆。
把位置 p 向后移动 n 个字节。（相关项：HSub、c、s、p、p - c、p - s。）
此段说明该操作的行为、边界条件及推荐用法。
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：Pos.Raw.unoffsetBy。）
从 p 中减去 offset。（相关项：HSub、c、s、p - c、p - s。）
此段说明该操作的行为、边界条件及推荐用法。
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：Pos.Raw.decreaseBy。）
创建一个新字符串，内容为输入字符串中由两个位置界定的区域。
位置或迭代器仅在满足所述边界与 UTF-8 字符边界条件时有效；无效输入的结果按说明处理。（相关项：""。）
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.extract、String.Slice、String.Slice.copy。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项：String.Pos.Raw.extract "red green blue" ⟨0⟩ ⟨3⟩ = "red"。）
示例见所列代码。（相关项：String.Pos.Raw.extract "red green blue" ⟨3⟩ ⟨0⟩ = ""。）
示例见所列代码。（相关项：String.Pos.Raw.extract "red green blue" ⟨0⟩ ⟨100⟩ = "red green blue"。）
示例见所列代码。（相关项：String.Pos.Raw.extract "red green blue" ⟨4⟩ ⟨100⟩ = "green blue"。）
示例见所列代码。（相关项：String.Pos.Raw.extract "L∃∀N" ⟨1⟩ ⟨2⟩ = "∃∀N"。）
示例见所列代码。（相关项：String.Pos.Raw.extract "L∃∀N" ⟨2⟩ ⟨100⟩ = ""。）
返回字符串位置 p 处的字符；若 p 无效，则返回后备值 (default : Char)，即 'A'，且不触发 panic。
运行时代码会用高效实现覆盖此函数。（相关项：String.Pos.Raw.utf8GetAux。）
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.Pos.get、String.pos、String.Pos。）
以下列出相应示例或例外情况。
返回字符串位置 p 处的字符；若 p 无效则触发 panic。
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：String.pos?、String.Pos.get。）
运行时代码会用高效实现覆盖此函数。（相关项：String.utf8GetAux。）
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.Pos.get、String.pos!、String.Pos。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项："abc".get! ⟨1⟩ = 'b'。）
返回字符串位置 p 处的字符；若 (default : Char) 无效，则返回 'A'，即 p。
此段说明该操作的行为、边界条件及推荐用法。（相关项：h、p、String.get。）
def getInBounds? (s : String) (p : String.Pos) : Option Char := if h : s.atEnd p then none else some (s.get' p h)
围栏之后的边界情况说明仍适用。（相关项：get'、if、¬ s.atEnd p。）
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：p、"L∃∀N".get' ⟨2⟩ (by decide) = (default : Char)、String.Pos.get。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项：String.pos。）
示例见所列代码。（相关项：String.Pos。）（相关项："abc".get' 0 (by decide) = 'a'、let lean := "L∃∀N"; lean.get' (0 |> lean.next |> lean.next) (by decide) = '∀'。）
返回字符串位置 p 处的字符；若 p 无效则返回 none。
运行时代码会用高效实现覆盖此函数。（相关项：String.utf8GetAux?。）
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.Pos.get、String.pos?、String.Pos。）
以下列出相应示例或例外情况。
用新字符替换字符串指定位置处的字符；若位置无效，则原样返回字符串。
若相关字符串未被共享，实现会尽可能进行原地更新而不复制。
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.Pos.set、String.pos、String.Pos。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项："abc".set ⟨1⟩ 'B' = "aBc"。）
示例见所列代码。（相关项："abc".set ⟨3⟩ 'D' = "abc"。）
示例见所列代码。（相关项："L∃∀N".set ⟨4⟩ 'X' = "L∃XN"。）
示例见所列代码。（相关项："L∃∀N".set ⟨2⟩ 'X' = "L∃∀N"、'∃'、2。）
以下列出相应示例或例外情况。
用 p 作用于该字符所得的结果替换字符串 s 中位置 f 处的字符；若 p 无效，则原样返回字符串。
若相关字符串未被共享，实现会尽可能进行原地更新而不复制。
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.Pos.set、String.pos、String.Pos。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项："abc".modify ⟨1⟩ Char.toUpper = "aBc"。）
示例见所列代码。（相关项："abc".modify ⟨3⟩ Char.toUpper = "abc"。）
选择字符串子区域（例如它的前缀或后缀）的操作会返回原字符串的一个切片，而不是分配一个新字符串。
使用 String.Slice.copy 将切片转换为新字符串。
返回包含 String.Slice 前 n 个字符（Unicode 码位）的 s。
在所述条件下，函数按说明返回相应结果或后备结果。（相关项：n、s.toList.length、s.toSlice。）
这是廉价操作，因为它不会为结果分配新字符串；需要字符串时可显式复制切片。（相关项：String.Slice.copy。）
示例：
String.takeWhile {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : String.SliceString.takeWhile {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : String.Slice
创建字符串切片，其中包含 s 中 pat 能够匹配（可能反复匹配）的最长前缀。
这是廉价操作，因为它不会为结果分配新字符串；需要字符串时可显式复制切片。（相关项：String.Slice.copy。）
此函数对当前支持的所有模式都是泛型的。
示例：
示例见所列代码。（相关项："red green blue".takeWhile Char.isLower == "red".toSlice。）
示例见所列代码。（相关项："red green blue".takeWhile 'r' == "r".toSlice。）
示例见所列代码。（相关项："red red green blue".takeWhile "red " == "red red ".toSlice。）
示例见所列代码。（相关项："red green blue".takeWhile (fun (_ : Char) => true) == "red green blue".toSlice。）
返回包含 String.Slice 后 n 个字符（Unicode 码位）的 s。
在所述条件下，函数按说明返回相应结果或后备结果。（相关项：n、s.toList.length、s.toSlice。）
这是廉价操作，因为它不会为结果分配新字符串；需要字符串时可显式复制切片。（相关项：String.Slice.copy。）
示例：
String.takeEndWhile {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : String.SliceString.takeEndWhile {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : String.Slice
创建字符串切片，其中包含 s 中 pat 能够匹配（可能反复匹配）的最长后缀。
这是廉价操作，因为它不会为结果分配新字符串；需要字符串时可显式复制切片。（相关项：String.Slice.copy。）
此函数对当前支持的所有模式都是泛型的。
示例：
示例见所列代码。（相关项："red green blue".takeEndWhile Char.isLower == "blue".toSlice。）
示例见所列代码。（相关项："red green blue".takeEndWhile 'e' == "e".toSlice。）
示例见所列代码。（相关项："red green blue".takeEndWhile (fun (_ : Char) => true) == "red green blue".toSlice。）
返回从字符串开头移除指定数量字符（Unicode 码位）后得到的 String.Slice。
在所述条件下，函数按说明返回相应结果或后备结果。（相关项：n、s.toList.length。）
这是廉价操作，因为它不会为结果分配新字符串；需要字符串时可显式复制切片。（相关项：String.Slice.copy。）
示例：
String.dropWhile {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : String.SliceString.dropWhile {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : String.Slice
创建字符串切片，其中从 s 移除了 pat 能够匹配（可能反复匹配）的最长前缀。
这是廉价操作，因为它不会为结果分配新字符串；需要字符串时可显式复制切片。（相关项：String.Slice.copy。）
此函数对当前支持的所有模式都是泛型的。
示例：
示例见所列代码。（相关项："red green blue".dropWhile Char.isLower == " green blue".toSlice。）
示例见所列代码。（相关项："red green blue".dropWhile 'r' == "ed green blue".toSlice。）
示例见所列代码。（相关项："red red green blue".dropWhile "red " == "green blue".toSlice。）
示例见所列代码。（相关项："red green blue".dropWhile (fun (_ : Char) => true) == "".toSlice。）
返回从字符串末尾移除指定数量字符（Unicode 码位）后得到的 String.Slice。
在所述条件下，函数按说明返回相应结果或后备结果。（相关项：n、s.toList.length。）
这是廉价操作，因为它不会为结果分配新字符串；需要字符串时可显式复制切片。（相关项：String.Slice.copy。）
示例：
String.dropEndWhile {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : String.SliceString.dropEndWhile {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : String.Slice
创建字符串切片，其中从 s 移除了 pat 能够匹配（可能反复匹配）的最长后缀。
这是廉价操作，因为它不会为结果分配新字符串；需要字符串时可显式复制切片。（相关项：String.Slice.copy。）
此函数对当前支持的所有模式都是泛型的。
示例：
示例见所列代码。（相关项："red green blue".dropEndWhile Char.isLower == "red green ".toSlice。）
示例见所列代码。（相关项："red green blue".dropEndWhile 'e' == "red green blu".toSlice。）
示例见所列代码。（相关项："red green blue".dropEndWhile (fun (_ : Char) => true) == "".toSlice。）
String.dropPrefix? {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : Option String.SliceString.dropPrefix? {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : Option String.Slice
若 pat 匹配 s 的前缀，则返回余下部分，否则返回 none。
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：String.dropPrefix、pat。）
这是廉价操作，因为它不会为结果分配新字符串；需要字符串时可显式复制切片。（相关项：String.Slice.copy。）
此函数对当前支持的所有模式都是泛型的。
示例：
示例见所列代码。（相关项："red green blue".dropPrefix? "red " == some "green blue".toSlice。）
示例见所列代码。（相关项："red green blue".dropPrefix? "reed " == none。）
示例见所列代码。（相关项："red green blue".dropPrefix? 'r' == some "ed green blue".toSlice。）
示例见所列代码。（相关项："red green blue".dropPrefix? Char.isLower == some "ed green blue".toSlice。）
String.dropPrefix {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : String.SliceString.dropPrefix {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : String.Slice
若 pat 匹配 s 的前缀，则返回余下部分，否则原样返回 s。
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：String.dropPrefix?、none、pat。）
这是廉价操作，因为它不会为结果分配新字符串；需要字符串时可显式复制切片。（相关项：String.Slice.copy。）
此函数对当前支持的所有模式都是泛型的。
示例：
示例见所列代码。（相关项："red green blue".dropPrefix "red " == "green blue".toSlice。）
示例见所列代码。（相关项："red green blue".dropPrefix "reed " == "red green blue".toSlice。）
示例见所列代码。（相关项："red green blue".dropPrefix 'r' == "ed green blue".toSlice。）
示例见所列代码。（相关项："red green blue".dropPrefix Char.isLower == "ed green blue".toSlice。）
String.dropSuffix? {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : Option String.SliceString.dropSuffix? {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : Option String.Slice
若 pat 匹配 s 的后缀，则返回余下部分，否则返回 none。
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：String.dropSuffix、pat。）
这是廉价操作，因为它不会为结果分配新字符串；需要字符串时可显式复制切片。（相关项：String.Slice.copy。）
此函数对当前支持的所有模式都是泛型的。
示例：
示例见所列代码。（相关项："red green blue".dropSuffix? " blue" == some "red green".toSlice。）
示例见所列代码。（相关项："red green blue".dropSuffix? "bluu " == none。）
示例见所列代码。（相关项："red green blue".dropSuffix? 'e' == some "red green blu".toSlice。）
示例见所列代码。（相关项："red green blue".dropSuffix? Char.isLower == some "red green blu".toSlice。）
String.dropSuffix {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : String.SliceString.dropSuffix {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : String.Slice
若 pat 匹配 s 的后缀，则返回余下部分，否则原样返回 s。
可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：String.dropSuffix?、none、pat。）
这是廉价操作，因为它不会为结果分配新字符串；需要字符串时可显式复制切片。（相关项：String.Slice.copy。）
此函数对当前支持的所有模式都是泛型的。
示例：
示例见所列代码。（相关项："red green blue".dropSuffix " blue" == "red green".toSlice。）
示例见所列代码。（相关项："red green blue".dropSuffix "bluu " == "red green blue".toSlice。）
示例见所列代码。（相关项："red green blue".dropSuffix 'e' == "red green blu".toSlice。）
示例见所列代码。（相关项："red green blue".dropSuffix Char.isLower == "red green blu".toSlice。）
返回起始位置为第一个非空白字符的切片，从而移除字符串开头的空白；若不存在非空白字符则以越尾位置为起点。
此段说明该操作的行为、边界条件及推荐用法。（相关项：Char.isWhitespace、true。）
示例：
示例见所列代码。（相关项："abc".trimAsciiStart == "abc".toSlice。）
示例见所列代码。（相关项：" abc".trimAsciiStart == "abc".toSlice。）
示例见所列代码。（相关项："abc \t ".trimAsciiStart == "abc \t ".toSlice。）
示例见所列代码。（相关项：" abc ".trimAsciiStart == "abc ".toSlice。）
示例见所列代码。（相关项："abc\ndef\n".trimAsciiStart == "abc\ndef\n".toSlice。）
返回结束位置为最后一个非空白字符之后的切片，从而移除字符串末尾的空白；若不存在非空白字符则以起始位置为终点。
此段说明该操作的行为、边界条件及推荐用法。（相关项：Char.isWhitespace、true。）
示例：
示例见所列代码。（相关项："abc".trimAsciiEnd == "abc".toSlice。）
示例见所列代码。（相关项：" abc".trimAsciiEnd == " abc".toSlice。）
示例见所列代码。（相关项："abc \t ".trimAsciiEnd == "abc".toSlice。）
示例见所列代码。（相关项：" abc ".trimAsciiEnd == " abc".toSlice。）
示例见所列代码。（相关项："abc\ndef\n".trimAsciiEnd == "abc\ndef".toSlice。）
一致地减少字符串各行的缩进：从每行开头移除相同数量的空白，使缩进最少的行不再有前导空白。
此段说明该操作的行为、边界条件及推荐用法。（相关项：' '、'\t'。）
此段说明该操作的行为、边界条件及推荐用法。
以下列出相应示例或例外情况。
示例见所列代码。（相关项："Here:\n fun x =>\n x + 1".removeLeadingSpaces = "Here:\nfun x =>\n x + 1"。）
示例见所列代码。（相关项："Here:\n\t\tfun x =>\n\t \tx + 1".removeLeadingSpaces = "Here:\nfun x =>\n \tx + 1"。）
示例见所列代码。（相关项："Here:\n\t\tfun x =>\n \n\t \tx + 1".removeLeadingSpaces = "Here:\nfun x =>\n\n \tx + 1"。）
String.find {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pattern : ρ) [String.Slice.Pattern.ToForwardSearcher pattern σ] : s.PosString.find {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pattern : ρ) [String.Slice.Pattern.ToForwardSearcher pattern σ] : s.Pos
String.revFind? {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pattern : ρ) [String.Slice.Pattern.ToBackwardSearcher pattern σ] : Option s.PosString.revFind? {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pattern : ρ) [String.Slice.Pattern.ToBackwardSearcher pattern σ] : Option s.Pos
String.contains {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pat : ρ) [String.Slice.Pattern.ToForwardSearcher pat σ] : BoolString.contains {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pat : ρ) [String.Slice.Pattern.ToForwardSearcher pat σ] : Bool
String.replace.{u_1} {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] {α : Type u_1} [String.ToSlice α] (s : String) (pattern : ρ) [String.Slice.Pattern.ToForwardSearcher pattern σ] (replacement : α) : StringString.replace.{u_1} {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] {α : Type u_1} [String.ToSlice α] (s : String) (pattern : ρ) [String.Slice.Pattern.ToForwardSearcher pattern σ] (replacement : α) : String
构造新字符串，把 pattern 中出现的所有 replacement 替换为 s。
此函数对当前支持的所有模式都是泛型的。（相关项：String、String.Slice。）
示例：
示例见所列代码。（相关项："red green blue".replace 'e' "" = "rd grn blu"。）
示例见所列代码。（相关项："red green blue".replace (fun c => c == 'u' || c == 'e') "" = "rd grn bl"。）
示例见所列代码。（相关项："red green blue".replace "e" "" = "rd grn blu"。）
示例见所列代码。（相关项："red green blue".replace "ee" "E" = "red grEn blue"。）
示例见所列代码。（相关项："red green blue".replace "e" "E" = "rEd grEEn bluE"。）
示例见所列代码。（相关项："aaaaa".replace "aa" "b" = "bba"。）
示例见所列代码。（相关项："abc".replace "" "k" = "kakbkck"。）
String.find {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pattern : ρ) [String.Slice.Pattern.ToForwardSearcher pattern σ] : s.PosString.find {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pattern : ρ) [String.Slice.Pattern.ToForwardSearcher pattern σ] : s.Pos
把函数 f 应用于字符串中的每个字符，并返回包含所得字符的字符串。
以下列出相应示例或例外情况。
示例见所列代码。（相关项："abc123".map Char.toUpper = "ABC123"。）
示例见所列代码。（相关项："".map Char.toUpper = ""。）
从开头折叠字符串，以 init 为初值，并用 f 按顺序把每个字符与累积值结合。
示例：
从右侧折叠字符串，以 init 为初值，并用 f 按逆序把每个字符与累积值结合。
示例：
检查字符串是否完全由模式 pat 的匹配组成。
遇到第一个决定结果的值时即短路，并按所述顺序检查元素。
此函数对当前支持的所有模式都是泛型的。
示例：
String.any {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pat : ρ) [String.Slice.Pattern.ToForwardSearcher pat σ] : BoolString.any {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pat : ρ) [String.Slice.Pattern.ToForwardSearcher pat σ] : Bool
LT String 实例是由基于 LT Char 实例的字符串字典序定义的。
在逻辑上，这是由对建模字符串的列表进行字典序排列来建模的，因此 List.Lex 定义了此顺序。
它是可判定的；在运行时，该判定过程会被利用字符串运行时表示的高效代码替代。
字符串上的非严格不等关系，通常通过运算符 ≤ 使用。
此段说明该操作的行为、边界条件及推荐用法。（相关项：a ≤ b、¬ b < a。）
返回两个字符串首次不同的位置。
在所述条件下，函数按说明返回相应结果或后备结果。
以下列出相应示例或例外情况。
示例见所列代码。（相关项："tea".firstDiffPos "ten" = ⟨2⟩。）
示例见所列代码。（相关项："tea".firstDiffPos "tea" = ⟨3⟩。）
示例见所列代码。（相关项："tea".firstDiffPos "teas" = ⟨3⟩。）
示例见所列代码。（相关项："teas".firstDiffPos "tea" = ⟨3⟩。）
检查第二个字符串（s）是否以某个前缀（p）开头。
此函数对当前支持的所有模式都是泛型的。
空串、前缀、后缀及越界情形按所述规则处理。（相关项：String.startsWith。）
示例：
示例见所列代码。（相关项："red".isPrefixOf "red green blue" = true。）
示例见所列代码。（相关项："green".isPrefixOf "red green blue" = false。）
示例见所列代码。（相关项："".isPrefixOf "red green blue" = true。）
String.startsWith {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : BoolString.startsWith {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : Bool
检查第一个字符串（s）是否以模式（pat）开头。
空串、前缀、后缀及越界情形按所述规则处理。（相关项：String.isPrefixOf。）
示例：
示例见所列代码。（相关项："red green blue".startsWith "red" = true。）
示例见所列代码。（相关项："red green blue".startsWith "green" = false。）
示例见所列代码。（相关项："red green blue".startsWith "" = true。）
示例见所列代码。（相关项："red green blue".startsWith 'r' = true。）
示例见所列代码。（相关项："red green blue".startsWith Char.isLower = true。）
检查字符串（s）是否以模式（pat）结尾。
此函数对当前支持的所有模式都是泛型的。
示例：
在 p 返回 true 的每个字符处拆分字符串。
空串、前缀、后缀及越界情形按所述规则处理。（相关项：p、p。）
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.split。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项："coffee tea water".split (·.isWhitespace) = ["coffee", "tea", "water"]。）
示例见所列代码。（相关项："coffee tea water".split (·.isWhitespace) = ["coffee", "", "tea", "", "water"]。）
示例见所列代码。（相关项："fun x =>\n x + 1\n".split (· == '\n') = ["fun x =>", " x + 1", ""]。）
在分隔字符串 s 每次出现的位置拆分字符串 sep；默认分隔符为 " "。
在所述条件下，函数按说明返回相应结果或后备结果。（相关项：sep、[s]、sep、n+1、n、sep。）
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.split。）
以下列出相应示例或例外情况。
把 s 的第一个字符替换为对它应用 Char.toUpper 的结果；若字符串为空则返回空字符串。
此段说明该操作的行为、边界条件及推荐用法。（相关项：Char.toUpper、'a'、'z'。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项："orange".capitalize = "Orange"。）
示例见所列代码。（相关项："ORANGE".capitalize = "ORANGE"。）
示例见所列代码。（相关项："".capitalize = ""。）
把 s 的第一个字符替换为对它应用 Char.toLower 的结果；若字符串为空则返回空字符串。
此段说明该操作的行为、边界条件及推荐用法。（相关项：Char.toLower、'A'、'Z'。）
以下列出相应示例或例外情况。
示例见所列代码。（相关项："Orange".decapitalize = "orange"。）
示例见所列代码。（相关项："ORANGE".decapitalize = "oRANGE"。）
示例见所列代码。（相关项："".decapitalize = ""。）
为了向后兼容，Lean 包含遗留的字符串迭代器。
从根本上说，一个 String.Legacy.Iterator 是一个字符串和该字符串中有效位置的有序对。
迭代器提供了获取当前字符（curr）、替换当前字符（setCurr）、检查迭代器是否可以向左或向右移动（分别为 hasPrev 和 hasNext），以及移动迭代器（分别为 prev 和 next）的函数。
调用者有责任检查它们是否已经到达字符串的开头或结尾；否则，迭代器确保其位置始终指向一个字符。
然而，String.Legacy.Iterator 不包含这些良构性条件的证明，这可能使其在经验证的代码中更难使用。
遍历 String 中字符（Unicode 码位）的迭代器，通常由 String.iter 创建。
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.Pos、s、p : s.startPos、p.next、p.get、p = s.endPos、p.IsAtEnd。）
位置或迭代器仅在满足所述边界与 UTF-8 字符边界条件时有效；无效输入的结果按说明处理。
位置或迭代器仅在满足所述边界与 UTF-8 字符边界条件时有效；无效输入的结果按说明处理。（相关项：i、s、0 ≤ i ≤ s.rawEndPos、i、i = s.rawEndPos。）
以下列出相应示例或例外情况。
以下列出相应示例或例外情况。（相关项：String.Iterator。）
示例见所列代码。（相关项：Iterator.next iter、iter、iter.atEnd。）
以下列出相应示例或例外情况。（相关项：true。）
示例见所列代码。（相关项：Iterator.forward iter n、Iterator.nextn iter n、n。）
以下列出相应示例或例外情况。
创建位于字符串开头的迭代器。
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.Pos、s、p : s.startPos、p.next、p.get、p = s.endPos、p.IsAtEnd。）
创建位于字符串开头的迭代器。
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.Pos、s、p : s.startPos、p.next、p.get、p = s.endPos、p.IsAtEnd。）
取得迭代器当前位置处的字符。
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.Pos、s、p : s.startPos、p.next、p.get、p = s.endPos、p.IsAtEnd。）
此段说明该操作的行为、边界条件及推荐用法。（相关项：String.Iterator.curr'。）
检查迭代器是否位于字符串最后一个字符处或其之前。
无条件把迭代器位置向前移动一个字符。
这是旧版 API，未来版本将移除；应优先使用所列的更安全替代方案。（相关项：String.Pos、s、p : s.startPos、p.next、p.get、p = s.endPos、p.IsAtEnd。）
位置或迭代器仅在满足所述边界与 UTF-8 字符边界条件时有效；无效输入的结果按说明处理。（相关项：Iterator.atEnd、false。）
String.Legacy.Iterator.next' (it : String.Legacy.Iterator) (h : it.hasNext = true) : String.Legacy.IteratorString.Legacy.Iterator.next' (it : String.Legacy.Iterator) (h : it.hasNext = true) : String.Legacy.Iterator
无条件把迭代器位置向前移动一个字符。
此段说明该操作的行为、边界条件及推荐用法。（相关项：it.hasNext、String.Iterator.next。）
把迭代器位置向前移动指定数量的字符。
位置或迭代器仅在满足所述边界与 UTF-8 字符边界条件时有效；无效输入的结果按说明处理。
把迭代器位置向前移动指定数量的字符。
位置或迭代器仅在满足所述边界与 UTF-8 字符边界条件时有效；无效输入的结果按说明处理。
检查迭代器是否已越过字符串开头。
无条件把迭代器位置向后移动一个字符。
此段说明该操作的行为、边界条件及推荐用法。
把迭代器位置向后移动指定数量的字符，并在字符串开头停止。
检查迭代器是否已越过其字符串的最后一个字符。
把迭代器位置移到字符串末尾，即最后一个字符之后。
替换字符串中的当前字符。
此段说明该操作的行为、边界条件及推荐用法。
String.Legacy.Iterator.find (it : String.Legacy.Iterator) (p : Char → Bool) : String.Legacy.IteratorString.Legacy.Iterator.find (it : String.Legacy.Iterator) (p : Char → Bool) : String.Legacy.Iterator
向前移动迭代器，直到布尔谓词 p 对当前字符返回 true，或到达字符串末尾；若当前字符已经满足 p，则不做任何操作。
String.Legacy.Iterator.foldUntil.{u_1} {α : Type u_1} (it : String.Legacy.Iterator) (init : α) (f : α → Char → Option α) : α × String.Legacy.IteratorString.Legacy.Iterator.foldUntil.{u_1} {α : Type u_1} (it : String.Legacy.Iterator) (init : α) (f : α → Char → Option α) : α × String.Legacy.Iterator
提取两个迭代器位置之间的子串；第一个位置为子串开头，第二个位置为子串结尾。
空串、前缀、后缀及越界情形按所述规则处理。
以字符串形式返回迭代器中余下的字符。
返回迭代器中余下的 UTF-8 字节数。
正在迭代的字符串。
某个底层字符串的区域或切片。
一个切片由一个字符串以及感兴趣区域的起始和结束字节位置组成。实际提取子字符串需要复制和内存分配，而同一个底层字符串的多个切片可以存在而几乎没有额外开销。虽然可以通过手动跟踪边界来实现，但切片 API 更加方便。
String.Slice 打包证明以确保起始和结束位置始终描绘出一个有效的字符串。出于这个原因，它应该优先于 Substring.Raw 使用。
构造子
String.Slice.mk
字段
str : String
底层字符串。
startInclusive : self.str.Pos
字符串切片开始的字节位置。
endExclusive : self.str.Pos
字符串切片结束的字节位置。
startInclusive_le_endExclusive : self.startInclusive ≤ self.endExclusive
该切片不是退化的（但它可能是空的）。
返回包含整个字符串的切片。
从p（包括）到s结束的切片。
从 s 的开头到 p（不含该位置）的切片。
A Slice.Pos s 是 s 中的一个字节偏移量，并附有证明该位置位于 UTF-8 字符边界处的证明。
字段
offset : String.Pos.Raw
Slice.Pos 的底层字节偏移。
isValidForSlice : String.Pos.Raw.IsValidForSlice s self.offset
证明 offset 对字符串切片 s 是有效的。
字符串切片的 UTF-8 编码字节数。
String.Slice.pos (s : String.Slice) (off : String.Pos.Raw) (h : String.Pos.Raw.IsValidForSlice s off) : s.PosString.Slice.pos (s : String.Slice) (off : String.Pos.Raw) (h : String.Pos.Raw.IsValidForSlice s off) : s.Pos
从一个位置和一个关于它有效性的证明构造一个在 s 上有效的位置。
从一个位置构造一个有效的位置 s，如果该位置无效则引发运行时错误。
切片的结束位置，作为 Pos.Raw。
给定一个切片和切片内的有效位置，通过将切片的起始位置替换为给定位置，获取同一底层字符串上的新切片。
给定一个切片和切片内的有效位置，通过将切片的末端替换为给定位置，在相同的底层字符串上获得一个新的切片。
String.Slice.slice (s : String.Slice) (newStart newEnd : s.Pos) (h : newStart ≤ newEnd) : String.SliceString.Slice.slice (s : String.Slice) (newStart newEnd : s.Pos) (h : newStart ≤ newEnd) : String.Slice
给定一个切片以及切片内的两个有效位置，获得一个由新边界形成的在相同基础字符串上的新切片。
给定一个切片和切片内的两个有效位置，获取由新边界形成的相同底层字符串上的新切片，如果给定的结束位置严格小于给定的起始位置，则触发运行时错误。
String.Slice.dropEndWhile {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : String.SliceString.Slice.dropEndWhile {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : String.Slice
创建一个新切片，包含 s 中 pat 匹配的最长后缀（可能重复匹配）。
示例：
"red green blue".toSlice.dropEndWhile Char.isLower == "red green ".toSlice
"red green blue".toSlice.dropEndWhile 'e' == "red green blu".toSlice
"red green blue".toSlice.dropEndWhile (fun (_ : Char) => true) == "".toSlice
String.Slice.dropPrefix {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : String.SliceString.Slice.dropPrefix {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : String.Slice
如果 pat 匹配 s 的前缀，则返回剩余部分；否则原样返回 s。
可使用 String.Slice.dropPrefix? 返回 none，以处理 pat 不匹配前缀的情况。
此函数适用于当前支持的所有模式。
示例：
"red green blue".toSlice.dropPrefix "red " == "green blue".toSlice
"red green blue".toSlice.dropPrefix "reed " == "red green blue".toSlice
"red green blue".toSlice.dropPrefix 'r' == "ed green blue".toSlice
"red green blue".toSlice.dropPrefix Char.isLower == "ed green blue".toSlice
String.Slice.dropPrefix? {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : Option String.SliceString.Slice.dropPrefix? {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : Option String.Slice
如果 pat 匹配 s 的前缀，则返回剩余部分；否则返回 none。
可使用 String.Slice.dropPrefix 原样返回切片，以处理 pat 不匹配前缀的情况。
此函数适用于当前支持的所有模式。
示例：
"red green blue".toSlice.dropPrefix? "red " == some "green blue".toSlice
"red green blue".toSlice.dropPrefix? "reed " == none
"red green blue".toSlice.dropPrefix? 'r' == some "ed green blue".toSlice
"red green blue".toSlice.dropPrefix? Char.isLower == some "ed green blue".toSlice
String.Slice.dropSuffix {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : String.SliceString.Slice.dropSuffix {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : String.Slice
如果 pat 匹配 s 的后缀，则返回剩余部分；否则原样返回 s。
可使用 String.Slice.dropSuffix? 返回 none，以处理 pat 不匹配后缀的情况。
此函数适用于当前支持的所有模式。
示例：
"red green blue".toSlice.dropSuffix " blue" == "red green".toSlice
"red green blue".toSlice.dropSuffix "bluu " == "red green blue".toSlice
"red green blue".toSlice.dropSuffix 'e' == "red green blu".toSlice
"red green blue".toSlice.dropSuffix Char.isLower == "red green blu".toSlice
String.Slice.dropSuffix? {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : Option String.SliceString.Slice.dropSuffix? {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : Option String.Slice
如果 pat 匹配 s 的后缀，则返回剩余部分；否则返回 none。
可使用 String.Slice.dropSuffix 原样返回切片，以处理 pat 不匹配后缀的情况。
此函数适用于当前支持的所有模式。
示例：
"red green blue".toSlice.dropSuffix? " blue" == some "red green".toSlice
"red green blue".toSlice.dropSuffix? "bluu " == none
"red green blue".toSlice.dropSuffix? 'e' == some "red green blu".toSlice
"red green blue".toSlice.dropSuffix? Char.isLower == some "red green blu".toSlice
String.Slice.dropWhile {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : String.SliceString.Slice.dropWhile {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : String.Slice
创建一个新切片，包含 s 的最长前缀，该前缀与 pat 匹配（可能重复匹配）。
示例：
String.Slice.takeEndWhile {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : String.SliceString.Slice.takeEndWhile {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : String.Slice
创建一个新切片，包含 s 的后缀前缀，其中 pat 匹配（可能重复）。
此函数适用于所有当前支持的模式。
示例：
"red green blue".toSlice.takeEndWhile Char.isLower == "blue".toSlice
"red green blue".toSlice.takeEndWhile 'e' == "e".toSlice
"red green blue".toSlice.takeEndWhile (fun (_ : Char) => true) == "red green blue".toSlice
String.Slice.takeWhile {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : String.SliceString.Slice.takeWhile {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : String.Slice
创建一个新切片，包含 s 的最长前缀，该前缀与 pat 匹配（可能重复匹配）。
此函数适用于所有当前支持的模式。
示例：
访问字符串切片的 UTF-8 编码中指定的字节。
在运行时，这个函数由高效的、常数时间的代码实现。
访问字符串切片的 UTF-8 编码中指定的字节，如果位置超出范围则会触发 panic。
获取大于或等于给定字节位置的最小有效位置。
获取严格大于给定字节位置的最小有效位置。
String.Slice.contains {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ToForwardSearcher pat σ] : BoolString.Slice.contains {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ToForwardSearcher pat σ] : Bool
String.Slice.startsWith {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : BoolString.Slice.startsWith {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : Bool
检查切片 (s) 是否以模式 (pat) 开头。
此函数适用于当前支持的所有模式。
示例：
"red green blue".toSlice.startsWith "red" = true
"red green blue".toSlice.startsWith "green" = false
"red green blue".toSlice.startsWith "" = true
"red green blue".toSlice.startsWith 'r' = true
"red green blue".toSlice.startsWith Char.isLower = true
String.Slice.endsWith {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : BoolString.Slice.endsWith {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] : Bool
String.Slice.all {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : BoolString.Slice.all {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] : Bool
String.Slice.find? {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ToForwardSearcher pat σ] : Option s.PosString.Slice.find? {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ToForwardSearcher pat σ] : Option s.Pos
String.Slice.revFind? {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ToBackwardSearcher pat σ] : Option s.PosString.Slice.revFind? {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ToBackwardSearcher pat σ] : Option s.Pos
String.Slice.split {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ToForwardSearcher pat σ] : Std.Iter String.SliceString.Slice.split {ρ : Type} {σ : String.Slice → Type} [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ToForwardSearcher pat σ] : Std.Iter String.Slice
在每个与模式 pat 匹配的子切片处拆分切片。
与模式匹配的子切片不会包含在任何结果子切片中。如果连续多个子切片匹配该模式，结果列表将包含空字符串。
此函数适用于所有当前支持的模式。
示例：
("coffee tea water".toSlice.split Char.isWhitespace).toStringList == ["coffee", "tea", "water"]
("coffee tea water".toSlice.split ' ').toStringList == ["coffee", "tea", "water"]
("coffee tea water".toSlice.split " tea ").toStringList == ["coffee", "water"]
("ababababa".toSlice.split "aba").toStringList == ["coffee", "water"]
String.Slice.splitInclusive {ρ : Type} {σ : String.Slice → Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ToForwardSearcher pat σ] : Std.Iter String.SliceString.Slice.splitInclusive {ρ : Type} {σ : String.Slice → Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ToForwardSearcher pat σ] : Std.Iter String.Slice
在每个匹配模式 pat 的子切片处拆分切片。与 split 不同，匹配的子切片会包含在每个子切片的末尾。
此函数适用于所有当前支持的模式。
示例：
("coffee tea water".toSlice.splitInclusive Char.isWhitespace).toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
("coffee tea water".toSlice.splitInclusive ' ').toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
("coffee tea water".toSlice.splitInclusive " tea ").toList == ["coffee tea ".toSlice, "water".toSlice]
("baaab".toSlice.splitInclusive "aa").toList == ["baa".toSlice, "ab".toSlice]
创建一个迭代器，用于遍历 s 中的所有行，并去除行结束字符 \r\n 或 \n。
示例：
"foo\r\nbar\n\nbaz\n".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]
"foo\r\nbar\n\nbaz".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]
"foo\r\nbar\n\nbaz\r".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]
通过将切片的结束位置移动到最后一个非空白字符来移除切片末尾的空白字符，如果没有非空白字符，则移动到其起始位置。
“空白字符”被定义为 Char.isWhitespace 返回 true 的字符。
示例：
"abc".toSlice.trimAsciiEnd == "abc".toSlice
" abc".toSlice.trimAsciiEnd == " abc".toSlice
"abc \t ".toSlice.trimAsciiEnd == "abc".toSlice
" abc ".toSlice.trimAsciiEnd == " abc".toSlice
"abc\ndef\n".toSlice.trimAsciiEnd == "abc\ndef".toSlice
通过将切片的起始位置移动到第一个非空白字符处（如果没有非空白字符，则移动到其结束位置），来移除切片开头的空白字符。
“空白字符”被定义为 Char.isWhitespace 返回 true 的字符。
示例：
"abc".toSlice.trimAsciiStart == "abc".toSlice
" abc".toSlice.trimAsciiStart == "abc".toSlice
"abc \t ".toSlice.trimAsciiStart == "abc \t ".toSlice
" abc ".toSlice.trimAsciiStart == "abc ".toSlice
"abc\ndef\n".toSlice.trimAsciiStart == "abc\ndef\n".toSlice
创建一个迭代器，用于遍历 {name}s 内的所有有效位置。
示例：
{lean}("abc".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', 'c']
{lean}("abc".toSlice.positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2]
{lean}("ab∀c".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', '∀', 'c']
{lean}("ab∀c".toSlice.positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2, 5]
创建一个迭代器，遍历 {name}s 中所有有效位置，从最后一个有效位置开始，向第一个位置迭代。
例子
{lean}("abc".toSlice.revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', 'b', 'a']
{lean}("abc".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [2, 1, 0]
{lean}("ab∀c".toSlice.revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', '∀', 'b', 'a']
{lean}("ab∀c".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [5, 2, 1, 0]
String.Slice.revSplit {σ : String.Slice → Type} {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ToBackwardSearcher pat σ] : Std.Iter String.SliceString.Slice.revSplit {σ : String.Slice → Type} {ρ : Type} (s : String.Slice) (pat : ρ) [String.Slice.Pattern.ToBackwardSearcher pat σ] : Std.Iter String.Slice
从切片末端向开头遍历，在每个与模式 pat 匹配的子切片处拆分切片。
与模式匹配的子切片不会包含在任何结果子切片中。如果多个连续子切片匹配该模式，结果列表将包含空切片。
此函数适用于当前支持的所有模式，但 String/String.Slice 除外。
示例：
从开始对切片上的函数进行折叠，从 init 开始累积值。累积的值按照顺序与每个字符结合，使用 f。
示例：
从末尾对切片上的函数进行折叠，累积一个从 init 开始的值。累积值按照逆序与每个字符结合，使用 f。
示例：
检查切片能否解释为自然数的十进制表示。
切片非空且其中所有字符都是数字时，便可解释为十进制自然数。为便于阅读，可以使用下划线 (_) 分隔数字，但下划线不能位于开头或结尾，也不能连续出现。
使用 toNat? 或 toNat! 将此类切片转换为自然数。
示例：
检查 s1 == s2 是否成立，如果忽略 ASCII 大小写。
字符串切片支持广义的搜索模式。 许多切片操作并不只针对字符或字符串定义，而是接受任意模式。 通过为本节中的类定义实例，可以让新的类型也成为模式。 Lean 标准库提供了实例，使下列类型既可用于向前搜索，也可用于向后搜索：
模式类型 | 含义 |
|---|---|
匹配给定字符 | |
匹配任意满足该谓词的字符 | |
匹配给定字符串的出现位置 | |
匹配该切片所表示字符串的出现位置 |
String.Slice.Pattern.ToForwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (String.Slice → Type)) : TypeString.Slice.Pattern.ToForwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (String.Slice → Type)) : Type
提供从模式到 SearchStep 迭代器的转换；该迭代器从 Slice 的开头向末尾搜索模式匹配项。
这些操作可以基于 ForwardPattern 实现，但某些模式可以采用更高效的实现。例如，String 模式搜索器若由字符串的 ForwardPattern 实例派生，就会尝试在字符串的每个位置匹配模式，而已有更高效的字符串匹配方法。Lean 标准库实际使用 Knuth–Morris–Pratt 算法；实现见模块 Init.Data.String.Pattern.String。
此类型类可用于提供这样的高效实现。如果不需要这种专门实现，可以使用 ToForwardSearcher.defaultImplementation 自动派生实例。
方法
toSearcher : (s : String.Slice) → Std.Iter (String.Slice.Pattern.SearchStep s)
构建一个迭代器，其产生的 SearchStep 对应于模式 pat 在切片
s 中的各次匹配。该迭代器返回的 SearchStep 所含范围必须
彼此相邻、互不重叠，并覆盖整个 s。
从 Slice 的起始提供简单的模式匹配功能。
方法
skipPrefix? : (s : String.Slice) → Option s.Pos
检查切片是否以该模式开始。如果是，则返回移除了前缀的切片；否则结果为 none。
skipPrefixOfNonempty? : (s : String.Slice) → s.isEmpty = false → Option s.Pos
检查切片是否以该模式开始。如果是，则返回移除了前缀的切片；否则结果为 none。
startsWith : String.Slice → Bool
检查切片是否以该模式开始。
String.Slice.Pattern.ToBackwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (String.Slice → Type)) : TypeString.Slice.Pattern.ToBackwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (String.Slice → Type)) : Type
提供从模式到 SearchStep 迭代器的转换；该迭代器从 Slice 的末尾向开头搜索模式匹配项。
这些操作可以基于 BackwardPattern 实现，但某些模式可以采用更高效的实现。例如，String 模式搜索器若由字符串的 BackwardPattern 实例派生，就会尝试在字符串的每个位置匹配模式，而已有更高效的字符串匹配方法。Lean 标准库实际使用 Knuth–Morris–Pratt 算法；实现见模块 Init.Data.String.Pattern.String。
此类型类可用于提供这样的高效实现。如果不需要这种专门实现，可以使用 ToBackwardSearcher.defaultImplementation 自动派生实例。
方法
toSearcher : (s : String.Slice) → Std.Iter (String.Slice.Pattern.SearchStep s)
构建一个迭代器，其产生的 SearchStep 对应于模式 pat 在切片
s 中的各次匹配。该迭代器返回的 SearchStep 所含范围必须
彼此相邻、互不重叠，并覆盖整个 s。
提供从Slice末尾进行简单模式匹配的功能。
方法
skipSuffix? : (s : String.Slice) → Option s.Pos
检查切片是否以该模式结束。如果是，则返回移除该后缀的切片；否则结果为 none。
skipSuffixOfNonempty? : (s : String.Slice) → s.isEmpty = false → Option s.Pos
检查切片是否以该模式结束。如果是，则返回移除该后缀的切片；否则结果为 none。
endsWith : String.Slice → Bool
检查切片是否以该模式结尾。
由于切片位置保留了对其来源切片的引用，因此可以借助它们查找单个字符或字节。
返回切片中某个位置的字节，该位置不是结束位置。
获取字符串中给定位置的字符。
返回字符串中给定位置的字节；如果该位置是结束位置，则引发运行时错误。
在给定一个证明该位置不是起始位置的前提下，返回给定位置之前的有效位置，这保证了这样的一个位置存在。
返回给定位置之前的上一个有效位置；如果给定位置是起始位置，则引发运行时错误。
在给定证明该位置不是超出末尾位置的情况下，将有效位置在切片上前进到下一个有效位置，这保证了该位置的存在。
将切片上的有效位置推进到下一个有效位置；如果给定位置是末端之后的位置，则引发运行时错误。
String.Slice.Pos.ofSlice {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} (pos : (s.slice p₀ p₁ h).Pos) : s.PosString.Slice.Pos.ofSlice {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} (pos : (s.slice p₀ p₁ h).Pos) : s.Pos
给定s.slice p₀ p₁ h中的一个位置，获得s中的对应位置。
原生子字符串是一种底层类型，它将字符串与其内部限定某个区域的字节位置组合在一起。 大多数代码应该改用切片，因为它们更安全也更方便。
某些底层字符串的区域或切片。
子字符串包含一个字符串以及感兴趣区域的起始和结束字节位置。实际上提取子字符串需要复制和内存分配，而同一底层字符串可能存在许多子字符串，开销很小，并且它们比手动跟踪边界更方便。
显式使用其构造函数，可以构造一个 Substring，其中一个或两个位置对于字符串无效。如果开始位置和停止位置无效，许多操作将返回意外或令人困惑的结果。因此，Substring 将被弃用，取而代之的是 String.Slice，它始终表示有效的子字符串。
构造子
Substring.Raw.mk
字段
str : String
底层字符串。
startPos : String.Pos.Raw
字符串切片起始位置的字节位置。
stopPos : String.Pos.Raw
字符串切片结束位置的字节位置。
检查子字符串是否为空。
如果子字符串的开始位置和结束位置相同，则子字符串为空。
字符串的 UTF-8 编码使用的字节数。
检查子字符串中的位置是否精确等于其结束位置。
该位置是相对于子字符串的起始位置而不是基础字符串的起始位置来理解的。
返回子字符串中给定位置之后的下一个位置。如果位置位于子字符串的末尾，则原样返回。
输入位置和返回位置都是相对于子字符串的起始位置而不是基础字符串进行解释的。
返回子字符串中从给定位置向前指定字符数的位置。如果到达子字符串的结束位置，则返回该子字符串。
输入位置和返回位置都是相对于子字符串的起始位置而不是基础字符串进行解释的。
返回子字符串中给定位置之前的上一个位置。如果位置位于子字符串的开头，则原样返回。
输入位置和返回位置都是相对于子字符串的起始位置而不是基础字符串进行解释的。
返回子字符串中给定位置之前指定字符数的位置。如果到达子字符串的起始位置，则返回该子字符串。
输入位置和返回位置都是相对于子字符串的起始位置而不是基础字符串进行解释的。
将函数折叠到左侧的子字符串上，累加以 init 开头的值。累加值按顺序与每个字符组合，使用 f。
将函数折叠到右侧的子字符串上，累加以 init 开头的值。使用 f 将累积值与每个字符按相反顺序组合。
检查两个子字符串是否表示相等的字符串。通常通过 == 运算符访问。
两个子字符串不需要具有相同的底层字符串或相同的开始和结束位置；相反，如果它们包含相同的字符序列，则它们相等。
检查两个子字符串是否具有相同的位置和内容。
两个子字符串不需要具有相同的基础字符串即可使此检查成功。
返回两个子字符串的最长公共前缀。
返回的子字符串使用与 s 相同的基础字符串。
返回两个子字符串的最长公共后缀。
返回的子字符串使用与 s 相同的基础字符串。
检查子字符串是否包含指定字符。
通过向前移动子字符串的起始位置，从子字符串的开头删除指定数量的字符（Unicode 代码点）。
如果到达子字符串的结束位置，则起始位置不会提前超过它。
通过将子字符串的结束位置移向其开始位置，从子字符串的末尾删除指定数量的字符（Unicode 代码点）。
如果到达子字符串的起始位置，则结束位置不会缩回超过它。
通过将子字符串的结束位置移向开始位置，仅保留子字符串开头的指定数量的字符（Unicode 代码点）。
如果到达子字符串的起始位置，则结束位置不会缩回超过它。
通过将子字符串的起始位置移向结束位置，仅保留子字符串末尾指定数量的字符（Unicode 代码点）。
如果到达子字符串的结束位置，则起始位置不会提前超过它。
以子字符串的形式返回由提供的开始位置和停止位置分隔的子字符串区域。这些位置是根据子字符串的起始位置而不是底层字符串来解释的。
如果生成的子字符串为空，则生成的子字符串是空字符串 "" 的子字符串。否则，底层字符串是输入子字符串的起始位置和结束位置已调整的字符串。
通过首先将其起始位置移动到第一个非空白字符，然后将其结束位置移动到最后一个非空白字符，从子字符串中删除前导和尾随空白。
如果子字符串仅包含空格，则生成的子字符串的起始位置将移动到其结束位置。
“空白”定义为 Char.isWhitespace 返回 true 的字符。
示例：
" red green blue ".toRawSubstring.trim.toString = "red green blue"
" red green blue ".toRawSubstring.trim.startPos = ⟨1⟩
" red green blue ".toRawSubstring.trim.stopPos = ⟨15⟩
" ".toRawSubstring.trim.startPos = ⟨5⟩
通过将子字符串的起始位置移动到第一个非空格字符，或者如果没有非空格字符，则移动到其结束位置，从而删除子字符串中的前导空格。
“空白”定义为 Char.isWhitespace 返回 true 的字符。
通过将子字符串的结束位置移动到最后一个非空格字符，或者如果没有非空格字符，则移动到其开始位置，从而删除子字符串中的尾随空格。
“空白”定义为 Char.isWhitespace 返回 true 的字符。
在子字符串 s 中每次出现分隔符字符串 sep 的位置进行拆分。默认分隔符是 " "。
当 sep 为空时，结果为 [s]。当 sep 以重叠模式出现时，采用首个匹配。如果存在 n+1 个返回元素，则恰好存在 n 个非重叠的 sep 匹配。分隔符不会包含在返回的子字符串中，而这些子字符串全都是 s 的底层字符串的子字符串。
给定一个 Substring，返回另一个具有有效端点并根据 Substring.toString 表示相同子字符串的值。 （注意，子字符串仍然可能是反转的，即开始大于结束。）
{} 将子字符串指向的基础字符串区域复制到新字符串中。
检查子字符串是否可以解释为自然数的十进制表示形式。
如果子字符串不为空并且其中的所有字符都是数字，则可以将其解释为十进制自然数。为了便于阅读，允许使用下划线 ({lit}_) 作为数字分隔符，但不能出现在开头、结尾或连续。
使用 Substring.toNat? 将此类子字符串转换为自然数。
检查子字符串是否可以解释为自然数的十进制表示形式，如果可以则返回该数字。
如果子字符串不为空并且其中的所有字符都是数字，则可以将其解释为十进制自然数。下划线 ({lit}_) 允许作为数字分隔符，但在解析过程中会被忽略。
使用Substring.isNat检查子串是否是这样的子串。
返回一个迭代器到底层字符串的子字符串的起始位置。结束位置被丢弃，因此不能单独使用迭代器来确定其当前位置是否在原始子字符串内。
将子字符串转换为 Lean 编译器中的名称表示。所得名称具有层级结构，字符串会在点号（'.'）处分段。
"a.b".toRawSubstring.toName 得到名称 a.b，而非 «a.b»。若要得到后者，请使用
Name.mkSimple ∘ Substring.Raw.toString。
-- 此旧名称计划弃用
把字符串转换为 Lean 编译器使用的名称表示；所得名称具有层次结构，并在点号（'.'）处拆分字符串。
此段说明该操作的行为、边界条件及推荐用法。（相关项："a.b".toName、a.b、«a.b»、Name.mkSimple。）
访问字符串 UTF-8 编码中指定的字节。
运行时代码会用高效实现覆盖此函数。
返回字符串的 UTF-8 编码所占的字节数。
运行时实现具有所述优化与复杂度特性。
返回字符的 UTF-8 编码中的字节序列。
把每个 \r\n 替换为 \n 以规范化行尾，但不检查是否存在孤立的 \r 字符。
此段说明该操作的行为、边界条件及推荐用法。（相关项：String.replace text "\r\n" "\n"。）
typedef struct {
lean_object m_header;
/* 字节长度，包含 '\0' 终止符 */
size_t m_size;
size_t m_capacity;
/* UTF8 长度 */
size_t m_length;
char m_data[0];
} lean_string_object;
这是字符串在 C 中的表示。更多细节参见 运行时 String 的说明。
bool lean_is_string(lean_object * o)
返回值为 true 当且仅当 o 是字符串；否则返回 false。
lean_string_object * lean_to_string(lean_object * o)
在运行时检查 o 是否确为字符串。若 o 不是字符串，则断言失败。