Isabelleでdataypeを定義する際にエラーが発生しました

Question

私はトポロジを使用する理論に取り組んでおり、オープンセットのタイプを持つと便利です。私は、次のことを試してみました：

トポロジーは、ロケールで、コンテキストコマンドが正しく出力に

locale topology = 
    fixes T :: "'a set set" 
    assumes "topology T" 

を与えるしかし、私は次のエラーを取得する

context topology 
begin 
typedef openset = "{U. U ∈ T}" 
end 

：

Extra type variables in representing set: "'a" The error(s) above occurred in typedef "openset"

それを何平均？ここでTは単なるセットであり、Tに属するセットを構成したいと考えていますが、これを行う方法はありますか？

Answer 1

まず、これはデータ型ではなく、通常の型定義です。

問題は、ロケールパラメータに依存する型定義を持つことができないことです。イザベルの論理的基盤は、現時点でそのようなことを許可していません。 Cf。この質問も：What Kind of Type Definitions are Legal in Local Contexts?