Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]

>>> Is there actually a drawback when using == instead of = or is it a mere
>>> matter of style? I like using Pure equality because it saves me a level
>>> of parentheses when I have a binder on the right hand side.
>> It is simpler:
>> a) Uniformity
>> b) Less symbols
> Ok, these are stylistic reasons and both only hold when always using =,
> and not <-> (<-> can be used for all of definition, primrec, fun(ction),
> but only for boolean valued functions. And I don't like it for
> definitions anyway ;)).

The matter <-> vs. = is orthogonal to == vs. =

>> Why care about »foo« anyway?

This should have read »Why care about »==« anyway?«.  The statement is
that end-users need not to even now about »==« in most situations (the
only exception known to me are rules like split_paired_All (all?) where
you rewrite framework-level connectives).  So why burden them with it?



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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