使用`o`作为变量/函数名称时出现内部语法错误

在与Isabelle（版本2016-1）一起玩时，我遇到了以下奇怪的情况：我不能使用字母o作为变量或函数名称（大部分/全部？）上下文。下面的例子都失败，尽管大部分工作（全部？）英文字母表的其他字母：使用`o`作为变量/函数名称时出现内部语法错误

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是一个保留名称，因此，这是一个bug或者是有一些o的其他用法排除它作为变量/函数名称？所有情况下的错误消息是“内部语法错误→解析语句失败”，除了注意到错误似乎与内部语法相关（第三个和最后一个错误消息出现在行中使用o而不是定义/有趣行）。

来源

2017-01-10 JAB

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

您可以使用命令

no_notation Fun.comp (infixl "o" 55)

你应该，但是，只能做禁用你的目的这用于实验;在生产使用中，禁用这种全球预定义符号会被认为是不好的。

我觉得这些日子里，这些旧的ASCII符号大多是不必要的，而且在o的情况下，实际上是有害的（例如它是如何混淆你的）。我会建议在Isabelle邮件列表中删除这个特殊符号。

来源

2017-01-10 06:58:25

那么这是有道理的。 'value '和'value '确实产生了相同的结果，并且使用有效的术语ctrl-单击'o'确实到达了“Fun.comp”的定义。 – JAB

fyi我在邮件列表中提出了这个问题，似乎共识似乎是我们想要删除'o'符号 - 然而，这个问题由于关系构成的相关“O”和“OO”符号而复杂一点。它们没有非ASCII表示法，并且不清楚可以用什么替代ASCII表示法。 –

我猜测有些限制/歧义可以防止由于它们对参数施加类型限制而导致over被重载为“o”和“O”？（尽管使用'OO'作为另一个标识符似乎比使用'o'或'O'更加不可靠的情况。） – JAB

使用`o`作为变量/函数名称时出现内部语法错误

回答

相关问题