類型導入似乎並沒有爲我工作在Isabelle2016

Question

我是一個完整的初學者Isabelle，我必須做錯了，因爲下面看似簡單的測試代碼只是不編譯我：

theory testit 
imports 
    "~~/src/HOL/Library/Inner_Product" 
begin 

    thm inner_zero_left 
    typ "real_inner" 
end 

在jedit界面中，thm命令似乎工作正常（所以它在Inner_Product導入中看到了定理），但real_inner類型不是。這是抱怨

Undefined type name: "real_inner"⌂ 
Failed to parse type 

我得到同樣的錯誤，如果我嘗試在定理中使用real_inner。

Answer 1

real_inner不是一種類型;這是一個類型類。如果您的意思是'一種類型類型real_inner'，則需要使用帶排序註釋的自由類型變量real_inner：

typ "'a :: real_inner"