[isabelle-dev] Unqualified swap?
florian.haftmann at informatik.tu-muenchen.de
Mon Apr 21 21:18:00 CEST 2014
See now http://isabelle.in.tum.de/reports/Isabelle/rev/6532efd66a70
On 12.04.2014 20:05, Tobias Nipkow wrote:
> Swap is a very generic name. There is already the qualified Fun.swap, but so
> far we did not seem to need one on pairs. Hence I would not introduce an
> unqualified swap on pairs now. If you find Product_Type.swap too heavy (but
> how often is it used?) you could call is swap_pair. But don't just call it swap.
> On 12/04/2014 19:02, Florian Haftmann wrote:
>> In 8f1e7596deb7 I have introduced
>> swap :: 'a * 'b => 'b * 'a
>> on products.
>> Is this common enough to be left unqualified? I hesitated to qualify it
>> since Product_Type.swap is too cumbersome (although something different
>> could be achieved using low-level namespace manipulation).
>> (One might ask whether the _Type suffix on Product_Type.thy (and Sum.thy
>> and some others in Library/) should be discontinued then, but this is
>> another question)
>> Any remarks? Florian
>> _______________________________________________ isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 263 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev