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?

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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