[isabelle-dev] Unqualified swap?
nipkow at in.tum.de
Sat Apr 12 20:05:21 CEST 2014
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
More information about the isabelle-dev