変数/関数名に `o`を使用したときの内部構文エラー

Question

Isabelle（バージョン2016-1）で遊んでいるときに、次のような奇妙な状況が発生しました。さまざまな変数または関数名として文字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を文書化する任意の情報を見つけるように見えることはできません変数/関数名として除外するoの他の使用法はありますか？すべてのケースのエラーメッセージは「内部構文エラーterm用語の解析に失敗しました」です。これは内部的な構文に関連しているように見えること以外はあまり役に立ちません（3番目と最後のケースのエラーメッセージはまた、定義/ fun行ではなく、引用符の内部にoを使用しています）。

Answer 1

oは、関数合成演算子∘のASCII表記です。 oは暗いターコイズ色で印刷され、他の識別子は青色、黒色、緑色またはオレンジ色（正確には何かに依存する）であるため、構文として解釈されることがわかります。あなたは、Oのような他の事前定義された構文でOO、powr、has_derivativeを、同じものを得るなど

あなたは

no_notation Fun.comp (infixl "o" 55) 

あなたは、しかし、唯一のやるべきコマンドを使用して、あなたの目的のためにそれを無効にすることができますこれは実験のためのものです。本番用では、このようなグローバルな事前定義表記を無効にすることは悪いと考えられます。

最近のこれらの古いASCII表記は、ほとんどが不要で、oの場合、実際には（たとえばあなたを混乱させるなどの）実際には有害であると思います。 Isabelleメーリングリストでこの特定の記法を削除することをお勧めします。