I’m not sure what to conclude from this. It’s about non-functional behaviour, so not quite something people ought to rely upon.
I’m guessing one could make the change and nothing would happen. I’m still not convinced that the case for a change has been made however. For what it’s worth, there are no such operators in HOL Light. Larry > On 22 Jan 2017, at 08:18, Florian Haftmann > <florian.haftm...@informatik.tu-muenchen.de> wrote: > > Surprisingly (?), there is no error here. The reason is obvious when > inspecting src/Pure/library.ML: > > ML ‹ > fun (f oo g) x y = f (g x y); > fun (f ooo g) x y z = f (g x y z); > fun (f oooo g) x y z w = f (g x y z w); > › > > The composition operators always wait for all arguments to be applied! > Alternative definitions would be > > ML ‹ > fun (f oo g) x = f o g x; > fun (f ooo g) x = f oo g x; > fun (f oooo g) x = f ooo g x; > › > > ML_val ‹ > fun foo k = error (string_of_int (k + 1)); > > val bar = I oo foo; > > val _ = bar 41; > › > > Yielding the expected error. > > I am not sure whether this is a striking argument to change such > long-standing definitions dating back to c755dfd02509 in 1998. But it is > at least worth noting that these are not apt for partial application. >
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
