使用 `o` 作为 variable/function 名称时出现内部语法错误

Question

我在玩Isabelle（2016-1版）的时候，遇到了以下奇怪的情况：在各种（most/all？）上下文。尽管适用于大多数（所有？）英语字母表中的其他字母，以下示例都失败了：

value o (* quoted version doesn't work either *)

definition invert :: ‹bool ⇒ bool› where
  ‹invert o = (¬ o)›

definition o :: ‹bool ⇒ bool› where
  ‹o a = (¬ a)›

fun default_int :: ‹int option ⇒ int› where
  ‹default_int None = 0› |
  ‹default_int o = the o›

fun default_int :: ‹int option ⇒ int› where
  ‹default_int None = 0› |
  ‹default_int (Some o) = o›

fun o :: ‹int option ⇒ int› where
  ‹o None = 0› |
  ‹o (Some i) = i›

我似乎找不到任何记录 o 是保留名称的信息，所以这是一个错误，还是 o 的其他用法导致它无法作为 variable/function姓名？所有情况的错误消息都是 "Inner syntax error⌂ Failed to parse term"，除了注意到错误似乎与内部语法相关（第三种和最后一种情况的错误消息出现在使用 o 在引号内，而不是在 definition/fun 行上。

Answer 1

o 是函数组合运算符 ∘ 的 ASCII 表示法。您可以看到 o 被解释为语法，因为它以一种深绿松石色打印，而其他标识符是蓝色、黑色、绿色或橙色（取决于它们的确切含义）。使用其他预定义语法，如 O、OO、powr、has_derivative 等，你会得到同样的结果

您可以使用命令

出于您的目的禁用它

no_notation Fun.comp (infixl "o" 55)

但是，您应该只为实验而这样做；在生产使用中，禁用这种全局预定义符号会被认为是不好的。

我认为这些天，这些旧的 ASCII 符号大多是不必要的，而且在 o 的情况下，实际上是有害的（例如它让你感到困惑）。我建议在 Isabelle 邮件列表中删除这个特殊的符号。

使用 `o` 作为 variable/function 名称时出现内部语法错误

Inner syntax error when using `o` as a variable/function name

isabelle