vars S, T : Type
types Bool;
Pred S := S ->? Unit;
Set S := S ->? Unit
ops True, False : Bool
ops emptySet : Set S;
{__} : S -> Set S;
__isIn__ : S * Set S ->? Unit;
__subset__ : Pred (Set (S) * Set (S));
__union__, __intersection__, __\\__ : Set S * Set S -> Set S;
__disjoint__ : Pred (Set (S) * Set (S));
__*__ : Set S * Set T -> Set (S * T);
__disjointUnion__ : Set S * Set S -> Set (S * Bool);
inl, inr : S -> S * Bool
forall x, x' : S; y : T; s, s' : Set S; t : Set T
. not x isIn emptySet
. x isIn { x' } <=> x = x'
. x isIn s <=> s x
. s subset s' <=> forall x : S . x isIn s => x isIn s'
. x isIn (s union s') <=> x isIn s \/ x isIn s'
. x isIn (s intersection s') <=> x isIn s /\ x isIn s'
. x isIn (s \\ s') <=> x isIn s /\ not x isIn s'
. s disjoint s' <=> s intersection s' = emptySet
. (x, y) isIn (s * t) <=> x isIn s /\ y isIn t
. inl x = (x, False)
. inr x = (x, True);
types
Bool : Type;
Set : Type -> Type
type
Set (S : Type) := S ->? Unit
vars
S : Type %(var_1)%;
T : Type %(var_2)%
op False : Bool
op True : Bool
op __*__ : forall S : Type; T : Type . Set S * Set T -> Set (S * T)
op __\\__ : forall S : Type . Set S * Set S -> Set S
op __disjoint__ : forall S : Type . Pred (Set S * Set S)
op __disjointUnion__ : forall S : Type
. Set S * Set S -> Set (S * Bool)
op __intersection__ : forall S : Type . Set S * Set S -> Set S
op __isIn__ : forall S : Type . S * Set S ->? Unit
op __subset__ : forall S : Type . Pred (Set S * Set S)
op __union__ : forall S : Type . Set S * Set S -> Set S
op emptySet : forall S : Type . Set S
op inl : forall S : Type . S -> S * Bool
op inr : forall S : Type . S -> S * Bool
op {__} : forall S : Type . S -> Set S
forall S : Type; x : S . not x isIn emptySet
forall S : Type; x : S; x' : S . x isIn { x' } <=> x = x'
forall S : Type; s : Set S; x : S . x isIn s <=> s x
forall S : Type; s : Set S; s' : Set S
. s subset s' <=> forall x : S . x isIn s => x isIn s'
forall S : Type; s : Set S; s' : Set S; x : S
. x isIn (s union s') <=> x isIn s \/ x isIn s'
forall S : Type; s : Set S; s' : Set S; x : S
. x isIn (s intersection s') <=> x isIn s /\ x isIn s'
forall S : Type; s : Set S; s' : Set S; x : S
. x isIn (s \\ s') <=> x isIn s /\ not x isIn s'
forall S : Type; s : Set S; s' : Set S
. s disjoint s' <=> s intersection s' = emptySet
forall S : Type; T : Type; s : Set S; t : Set T; x : S; y : T
. (x, y) isIn (s * t) <=> x isIn s /\ y isIn t
forall S : Type; x : S . inl x = (x, False)
forall S : Type; x : S . inr x = (x, True)
1.6: ### Hint: is type variable 'S'
1.9: ### Hint: is type variable 'T'
3.14: ### Hint: rebound type variable 'S'
3.8-3.11: ### Hint: redeclared type 'Pred'
4.13: ### Hint: rebound type variable 'S'
9.18: ### Hint:
no kind found for 'S'
expected: {Cpo}
found: {Type}
9.18: ### Hint:
no kind found for 'S'
expected: {Cppo}
found: {Type}
10.27-10.32: ### Hint:
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
10.27-10.32: ### Hint:
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
11.47-11.51: ### Hint:
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
11.47-11.51: ### Hint:
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
11.47-11.51: ### Hint:
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
11.47-11.51: ### Hint:
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
11.47-11.51: ### Hint:
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
11.47-11.51: ### Hint:
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
12.29-12.34: ### Hint:
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
12.29-12.34: ### Hint:
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
13.17-13.21: ### Hint:
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
13.17-13.21: ### Hint:
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
13.39: ### Hint:
no kind found for 'S'
expected: {Cpo}
found: {Type}
13.39: ### Hint:
no kind found for 'S'
expected: {Cppo}
found: {Type}
14.27-14.31: ### Hint:
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
14.27-14.31: ### Hint:
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
14.49: ### Hint:
no kind found for 'S'
expected: {Cpo}
found: {Type}
14.49: ### Hint:
no kind found for 'S'
expected: {Cppo}
found: {Type}
15.23: ### Hint:
no kind found for 'S'
expected: {Cpo}
found: {Type}
15.23: ### Hint:
no kind found for 'S'
expected: {Cppo}
found: {Type}
15.23: ### Hint:
no kind found for 'S'
expected: {Cpo}
found: {Type}
15.23: ### Hint:
no kind found for 'S'
expected: {Cppo}
found: {Type}
16.11: ### Hint: not a class 'S'
16.16: ### Hint: not a class 'S'
16.23: ### Hint: not a class 'T'
16.29: ### Hint: not a kind 'Set (S)'
16.34: ### Hint: not a kind 'Set (S)'
16.47: ### Hint: not a kind 'Set (T)'
20.33: ### Hint: not a class 'S'
20.31: ### Hint: rebound variable 'x'