[isabelle-dev] Unqualified swap?

[Florian Haftmann]

See now http://isabelle.in.tum.de/reports/Isabelle/rev/6532efd66a70

	Florian

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.
> 
> Tobias
> 
> 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 
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140421/3c706e1e/attachment.sig>