2013-10-28 2 views
1

를 제거 할 때 합금에 다음과 같은 사양을 고려 빈 세트를 가져옵니다 :합금 - 객체

우리가 대학 = {책 $ 0 책 $ 1, 책 $ 2} $을 $있는 인스턴스를 가지고 있다고 가정
sig Books {} 
fun f[b:Books] : Books { 

    {b':Books | b' = Books -b } 
} 
run show {} 

. $ 0 $ 대신 $ {책 $ 1, 책 $ 2}의 빈 세트 $ 책 f를 함수를 산출 평가 $ :

f[Books$0] 
{} 

왜 어떤 아이디어가?

답변

3

설정 방법에 대한 이해가 작동합니다.

{b':Books | b' = Books - b } 

이 식은 Books - b 동등한 Books 모든 싱글 서브 세트들을 전달한다. 그러나 Books - b은 두 요소 세트입니다. 따라서 어떤 싱글 톤 세트도 그와 동일하지 않으며 전체 결과는 {}입니다.

당신은 아마 단순히 원하는 :

fun f[b:Books] : Books { 
    Books - b 
}