Re: [isabelle] Syntax for Min/Max, or the notation for images

Well, a strong argument against any fancy syntax for image is that it would be input-only. Image is just an ordinary infix operator and the user would see something like a`i instead of {a i. i ∈ I}.

Users (especially beginners) should be aware that a general comprehension could give rise to a large formula. I frequently write expressions using nested unions instead. I don't know whether it really simplifies reasoning steps, but I find it clearer.


> On 19 Feb 2018, at 06:58, Tobias Nipkow <nipkow at> wrote:
> Using a standard set-comprehension syntax for image is plain misleading and will create more confusion (even if we manage to resolve the ambiguity that Andreas pointed out).
> Tobias

Attachment: signature.asc
Description: Message signed with OpenPGP

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