Email Gateway (Aug 22 2022 at 13:37): Email Gateway (Aug 22 2022 at 13:37):From: Omar Jasim <oajasim1@sheffield.ac.uk>
Deat list,
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.
Regards
Omar
Email Gateway (Aug 22 2022 at 13:37):From: Peter Lammich <lammich@in.tum.de>
Hi,
from your description its not clear what the operator should do.
But if you know the type signature (or parts of it), you can use the
query panel (find constants) to search for constants that match your
type signature.
The query "_*_ set" yields too many results for me, but maybe you can
refine it, e.g. "_*_ set -> <whatsoever>"
Email Gateway (Aug 22 2022 at 13:37):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Omar,
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,
Andreas
Last updated: Apr 25 2024 at 08:20 UTC