escaping - 为什么 '\SO' 的行为与 Agda 中的其他转义码不同？

Question

似乎我可以通过它的转义码来定义一个字符，比如

mychar : Char
mychar = '\US'

但不适用于 '\SO'，因为

mychar : Char
mychar = '\SO'

给

Lexical error in string or character literal: bad escape code

即使 Data.Char.show '\14'回馈 "'\\SO'" ，所以我不明白为什么它不应该工作。
它是否与“\SOH”的存在有某种关系？以 Agda 也可以读取的方式打印任何字符的最佳方法是什么？

Answer 1

这看起来像是 Agda 解析器中的一个错误，so I've reported it as such .特别是the match function不适用于非无前缀的情况，例如 SO对比 SOH .为了说明，这里有一个简短的例子:

λ» M.parse defaultParseFlags [] (runLookAhead error $ match [("FO", pure 1), ("FOO", pure 2)] (pure 3)) "FOO"
ParseOk (PState {parseSrcFile = Nothing, parsePos = Pn {srcFile = (), posPos = 1, posLine = 1, posCol = 1}, parseLastPos = Pn {srcFile = (), posPos = 1, posLine = 1, posCol = 1}, parseInp = "FOO", parsePrevChar = '\n', parsePrevToken = "", parseLayout = [NoLayout], parseLexState = [], parseFlags = ParseFlags {parseKeepComments = False}}) 2
λ» M.parse defaultParseFlags [] (runLookAhead error $ match [("FO", pure 1), ("FOO", pure 2)] (pure 3)) "FOB"
ParseOk (PState {parseSrcFile = Nothing, parsePos = Pn {srcFile = (), posPos = 1, posLine = 1, posCol = 1}, parseLastPos = Pn {srcFile = (), posPos = 1, posLine = 1, posCol = 1}, parseInp = "FOB", parsePrevChar = '\n', parsePrevToken = "", parseLayout = [NoLayout], parseLexState = [], parseFlags = ParseFlags {parseKeepComments = False}}) 3
λ» M.parse defaultParseFlags [] (runLookAhead error $ match [("FO", pure 1), ("FOO", pure 2)] (pure 3)) "FO"
*** Exception: unexpected end of file
CallStack (from HasCallStack):
  error, called at <interactive>:31:44 in interactive:Ghci8

如我们所见，如果我们有 "FO"和 "FOO"作为两种情况，解析 "FOO"按预期工作(返回 2)，解析 "FOB"按预期工作(从默认情况返回 3)，但输入 "FO"导致解析错误。