[isabelle-dev] Unqualified swap?

[Tobias Nipkow]

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
>