| Line | |
|---|
| 1 | var S,T : Type |
|---|
| 2 | type Bool; |
|---|
| 3 | Pred := \ (S: -Type) . S ->? Unit ; |
|---|
| 4 | Set := \ S:Type . S ->? Unit ; |
|---|
| 5 | ops True, False : Bool; |
|---|
| 6 | |
|---|
| 7 | ops emptySet : Set S; |
|---|
| 8 | {__} : S -> Set S; |
|---|
| 9 | __isIn__ : S * Set S ->? Unit; |
|---|
| 10 | __subset__ :Pred( Set(S) * Set(S) ); |
|---|
| 11 | __union__, __intersection__, __\\__ : Set S * Set S -> Set S; |
|---|
| 12 | __disjoint__ : Pred( Set(S) * Set(S) ); |
|---|
| 13 | __*__ : Set S * Set T -> Set (S*T); |
|---|
| 14 | __disjointUnion__ : Set S * Set S -> Set (S*Bool); |
|---|
| 15 | inl,inr : S -> S*Bool; |
|---|
| 16 | forall x,x':S; y:T; s,s':Set(S); t:Set(T) |
|---|
| 17 | . not (x isIn emptySet) |
|---|
| 18 | . (x isIn {x'}) <=> x=x' |
|---|
| 19 | . (x isIn s) <=> (s x) |
|---|
| 20 | . (s subset s') <=> (forall x:S . x isIn s => x isIn s') |
|---|
| 21 | . x isIn (s union s') <=> x isIn s \/ x isIn s' |
|---|
| 22 | . x isIn (s intersection s') <=> x isIn s /\ x isIn s' |
|---|
| 23 | . x isIn (s \\ s') <=> x isIn s /\ not x isIn s' |
|---|
| 24 | . s disjoint s' <=> s intersection s' = emptySet |
|---|
| 25 | . (x,y) isIn (s * t) <=> x isIn s /\ y isIn t |
|---|
| 26 | . inl x = (x,False) |
|---|
| 27 | . inr x = (x,True) |
|---|
