# IRC log for #isabelle, 2016-06-04

All times shown according to UTC.

Time Nick Message
01:47 ilbot3 joined #isabelle
01:47 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
01:55 fracting joined #isabelle
02:17 fracting joined #isabelle
06:01 fracting joined #isabelle
08:05 silver joined #isabelle
18:15 silver joined #isabelle
19:51 JCaesar Say, if I want to sort a list by a criterium comparing two elements, do I really have to define an ordering on them?
20:07 tangentstorm JCaesar: how can you sort something without defining an order?
20:13 JCaesar By giving an ordering criterin. What I'm saying is that I don't necesarily want this order to be associated with that type…
20:20 tangentstorm oh.
20:21 tangentstorm well a lot of languages offer a 'sortBy' that takes a list of xs and a function x->x->bool or x->x->(-1|0|1)
20:22 tangentstorm no idea whether isabelle offers anything like that.
20:34 JCaesar It doesn't seem like it, to me… I asked to see if I was wrong.
20:37 tangentstorm hrm. maybe there's some way to define a new temporary type that's a composition of the old one with whatever ordering function you want?
21:27 JCaesar That should be possible. But It's an awfully complicated way to implement sortBy, no?
21:40 ThreeOfEight I think there's something like that somewhere
21:40 ThreeOfEight merge sort or quick sort or something like that
21:40 ThreeOfEight something like sort_with_key
21:41 ThreeOfEight Ah, there you go. sort_key.
21:41 ThreeOfEight "sort" is actually just an abbreviation for "sort_key (λx. x)"
21:52 larsrh Doesn't sound like what JCaesar want though
21:53 JCaesar ThreeOfEight: I want a comparison function (i.e., a binary one), not a projection function.