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

如何解决为什么 '\SO' 的行为与 Agda 中的其他转义码不同？

好像可以通过转义码来定义一个字符，比如

mychar : Char
mychar = '\US'

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

mychar : Char
mychar = '\SO'

给予

字符串或字符文字中的词法错误：错误的转义码

即使 Data.Char.show '\14' 返回 "'\\SO'"，所以我不明白为什么它不应该起作用。

它是否与'\SOH'的存在有某种关系？以 Agda 也可以读取的方式打印任何字符的最佳方法是什么？

解决方法

这看起来像是 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 = (),parseInp = "FOO",parsePrevChar = '\n',parsePrevToken = "",parseLayout = [NoLayout],parseLexState = [],parseFlags = ParseFlags {parseKeepComments = False}}) 2
λ» M.parse defaultParseFlags [] (runLookAhead error $ match [("FO",pure 2)] (pure 3)) "FOB"
ParseOk (PState {parseSrcFile = Nothing,parseInp = "FOB",parseFlags = ParseFlags {parseKeepComments = False}}) 3
λ» M.parse defaultParseFlags [] (runLookAhead error $ match [("FO",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" 导致解析错误。