Direct definition of Theories Operators must be done in one single large predicate.
Would it be possible to specify several definitions and join them with an &?
Hi Luis Diaz,
I assume that you would like to have several operator definitions for each part of the large predicate and using them to define your operator. The following seems to work fine for me.
THEORY
Theory
OPERATORS
•myOp1 : myOp1(S : ℙ(ℤ)) PREDICATE PREFIX
direct definition
myOp1(S : ℙ(ℤ)) ≙ S ⊆ ℕ
•myOp2 : myOp2(S : ℙ(ℤ)) PREDICATE PREFIX
direct definition
myOp2(S : ℙ(ℤ)) ≙ (∀s·s ∈ S ⇒ s ≤ 5)
•myOp : myOp(S : ℙ(ℤ)) PREDICATE PREFIX
direct definition
myOp(S : ℙ(ℤ)) ≙ myOp1(S) ∧ myOp2(S)
END
I am not so sure if this style meets your expectation though.
Best,
Son
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Hi Luis Diaz,
I assume that you would like to have several operator definitions for each part of the large predicate and using them to define your operator. The following seems to work fine for me.
THEORY
Theory
OPERATORS
•myOp1 : myOp1(S : ℙ(ℤ)) PREDICATE PREFIX
direct definition
myOp1(S : ℙ(ℤ)) ≙ S ⊆ ℕ
•myOp2 : myOp2(S : ℙ(ℤ)) PREDICATE PREFIX
direct definition
myOp2(S : ℙ(ℤ)) ≙ (∀s·s ∈ S ⇒ s ≤ 5)
•myOp : myOp(S : ℙ(ℤ)) PREDICATE PREFIX
direct definition
myOp(S : ℙ(ℤ)) ≙ myOp1(S) ∧ myOp2(S)
END
I am not so sure if this style meets your expectation though.
Best,
Son