Isabelle - 字符和字符串文字支持
Isabelle - character and string literal support
在 Isabelle 中如何声明字符和字符串文字？我想在 Isabelle 教程的 trie 示例中使用字符节点值（声明为 'v option）。
datatype ('a,'v)trie = Trie "'v option" "('a * ('a,'v)trie)list"
有char类型，表示8位字符，还有string类型，定义为字符列表。还有一些用于字符和字符串文字的语法和漂亮的打印设置：
typ string
(* char list *)
term "''foobar''"
(* ''foobar'' :: char list *)
value "hd ''foobar''"
(* CHR ''f'' :: char *)
请注意，字符串文字必须用两个单引号分隔 ''。字符文字必须输入为 CHR ''c''。这目前适用于大多数可打印的 ASCII 字符，但不能超过 0x7F.
有函数nat_of_char和char_of_nat可以在这些8位字符和它们的ANSI代码（表示为nat）之间进行转换。
还有类型String.literal，它本质上是string的类型克隆，隐藏了底层的列表性质。这主要对代码生成很有趣，因为目标语言（例如 Scala）可能会提供专用的字符串类型（而不是仅仅一个字符列表）。 string 和 String.literal 之间的转换是 implode 和 explode。
请注意，如果您想使用字符串导出代码，您可能应该导入 ~~/src/HOL/Library/Code_Char.thy 以将 Isabelle 的字符类型转换为目标语言的字符类型。即便如此，使用 string 导出代码将导致代码使用字符列表；您需要在 Isabelle 代码方程中明确使用 String.literal 才能在 SML、Scala 和 OCaml 中获得正确的字符串类型。
有一些关于泛化 Isabelle 的字符类型以支持多字节字符的想法，但这仍然是未来的事情。
在 Isabelle 中如何声明字符和字符串文字？我想在 Isabelle 教程的 trie 示例中使用字符节点值（声明为 'v option）。
datatype ('a,'v)trie = Trie "'v option" "('a * ('a,'v)trie)list"
有char类型，表示8位字符，还有string类型，定义为字符列表。还有一些用于字符和字符串文字的语法和漂亮的打印设置：
typ string
(* char list *)
term "''foobar''"
(* ''foobar'' :: char list *)
value "hd ''foobar''"
(* CHR ''f'' :: char *)
请注意，字符串文字必须用两个单引号分隔 ''。字符文字必须输入为 CHR ''c''。这目前适用于大多数可打印的 ASCII 字符，但不能超过 0x7F.
有函数nat_of_char和char_of_nat可以在这些8位字符和它们的ANSI代码（表示为nat）之间进行转换。
还有类型String.literal，它本质上是string的类型克隆，隐藏了底层的列表性质。这主要对代码生成很有趣，因为目标语言（例如 Scala）可能会提供专用的字符串类型（而不是仅仅一个字符列表）。 string 和 String.literal 之间的转换是 implode 和 explode。
请注意，如果您想使用字符串导出代码，您可能应该导入 ~~/src/HOL/Library/Code_Char.thy 以将 Isabelle 的字符类型转换为目标语言的字符类型。即便如此，使用 string 导出代码将导致代码使用字符列表；您需要在 Isabelle 代码方程中明确使用 String.literal 才能在 SML、Scala 和 OCaml 中获得正确的字符串类型。
有一些关于泛化 Isabelle 的字符类型以支持多字节字符的想法，但这仍然是未来的事情。