Isabelle에서 dataype를 정의하는 중 오류가 발생했습니다.

Question

토폴로지를 사용하는 이론을 연구 중이므로 열린 세트 유형을 사용하는 것이 좋습니다.

이

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

토폴로지 로케일 올바르게 컨텍스트 명령입니다

이

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

는 그러나, 나는 다음과 같은 오류 얻을 출력을 제공합니다 : 나는이 다음 시도

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

무엇을합니까 평균? 여기서 T는 세트의 집합이며 T에 속한 세트로 구성된 유형을 갖고 싶습니다. 이것이 수행 될 수있는 방법이 있습니까?

Answer 1

우선, 이것은 데이터 유형이 아니며 '일반적인'유형 정의입니다.

문제는 로케일 매개 변수에 의존하는 유형 정의를 가질 수 없다는 것입니다. 이사벨 (Isabelle)의 논리적 토대는 그 순간에 그러한 것을 허용하지 않습니다. Cf. 또한이 질문 : What Kind of Type Definitions are Legal in Local Contexts?