Re: [isabelle] Relation of function absent from Main



It doesn't sound like a bad idea, and I seem to remember that I once toyed with adding it, but the fact that nobody ever added it indicates that it may not be worth it, i.e. that you can work with the set comprehension just as easily. But that is not clear.

Tobias

On 19/02/2021 18:38, Christian Pardillo Laursen wrote:
Hello,

I have been using the following function extensively:

definition rel_of :: "('a ⇒ 'a) ⇒ 'a rel" where "rel_of f = {(x,y) . f x = y}"

This seems to be absent from the Isabelle libraries, despite being obvious. Am I missing something, or is it perhaps a bad idea to convert between functions and relations?

Best regards,
Christian Pardillo Laursen

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.