Re: [isabelle] Operator with Pair sets
Do you want to have an operator from 'a * ('b set) to 'c * ('d set) or from ('a * 'b) set
to ('c * 'd) set? The first parenthesation corresponds to what you have written, but the
second version looks more like what I would expect from a "pair set". In case of the
latter, the theory Relation defines a number of useful operators, e.g., composition,
image, domain and range.
Hope this helps,
On 16/06/16 10:38, Omar Jasim wrote:
I want to ask if there is a theory state that there is an operator map from
pair set ('a x 'b set) to another pair set ('cx'd set) or I should define
it? if there are such related theories please could you give me their names.
This archive was generated by a fusion of
Pipermail (Mailman edition) and