區域設置進口兩類

我想定義的類和語言環境，並結合然後創建不同類型的我試圖通過區域設置進口兩類

theory Scratch 
imports Main 
begin 
class A = 
    fixes getA:: "'a ⇒ string" 

class B = 
    fixes getB:: "'a ⇒ string" 

locale CombAB = A + B + 
    fixes get:: "'a ⇒ string" 
end

結果給出的是

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"

爲什麼有三個變量'a,'b,'c而不只是一個？

來源

2016-09-13 Johan

除非另有說明，Isabelle總是派生出大多數一般類型。在這個特定的例子中，它不知道A，B和CombAB正在談論相同類型'a，所以它只是將類型變量重命名爲新的。您可以通過使用子句for明確指定所需類型來使用相同類型變量，如下所示：

locale CombAB = 
    A getA + 
    B getB 
    for 
     getA:: "'a ⇒ string" and 
     getB:: "'a ⇒ string" + 
    fixes 
     get:: "'a ⇒ string"

來源

2016-09-14 04:50:46

區域設置進口兩類

回答

相關問題