ロケールのインポート二つのクラス

Question

は

locale CombAB = 
    fixes getA :: "'b ⇒ char list" 
    and getB :: "'c ⇒ char list" 
    and get :: "'a ⇒ char list" 

ですが、私は

locale CombAB = 
fixes getA :: "'a ⇒ char list" 
    and getB :: "'a ⇒ char list" 
    and get :: "'a ⇒ char list" 

を期待しました

なぜ3つの変数'a,'b,'cがありますか？

Answer 1

特に断りのない限り、Isabelleは常に最も一般的な型を導出します。この特定の例では、A,BおよびCombABが同じタイプの'aを話しているとは考えられないので、タイプ変数の名前を新しいものに変更するだけです。次のように、句forで明示的に必要な型を指定して、同じ型変数を使用するように指定することができます。