Email Gateway (Mar 28 2021 at 09:21): Email Gateway (Mar 28 2021 at 09:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
I stumbled over an ancient combinator dating back to 2005.
There is the »modifying swap«
‹Fun.swap a b f = f (a := f b, b:= f a)›
However most applications need the canonical swap
‹swap a b x = (if x = a then b else if x = b then a else x)›
and help themselves by writing
‹Fun.swap a b id›
hence avoiding the pain to introduce another combinator.
for that.
Given that the modifying swap can simply expressed as (*)
‹Fun.swap a b f = f o swap a b›
it is tempting to change Fun.swap to the canonical swap and replace
remaining occurrences of the modifying swap using (*).
Any suggestions?
Florian
OpenPGP_signature
Email Gateway (Mar 28 2021 at 14:34):From: Lawrence Paulson <lp15@cam.ac.uk>
Sounds good to me! It’s good to reduce the number of easily inter-definable primitives.
Larry
Email Gateway (May 22 2021 at 06:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
To conclude this thread: this will be part of the next Isabelle release.
Florian
OpenPGP_signature
Last updated: Jan 04 2025 at 20:18 UTC