IRC log for #isabelle, 2017-08-02

All times shown according to UTC.

Time Nick Message
01:51 ilbot3 joined #isabelle
01:51 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/
02:30 https_GK1wmSU joined #isabelle
02:31 https_GK1wmSU left #isabelle
06:23 juanbono joined #isabelle
06:31 juanbono joined #isabelle
07:27 juanbono joined #isabelle
09:00 chindy Is there something like ordered sets, or would that just be lists?
09:01 larsrh !term ordered_set_of_list
09:01 isabelle-bot larsrh: ordered_set_of_list :: 'a
09:01 larsrh !term ordered_list_of_set
09:01 isabelle-bot larsrh: ordered_list_of_set :: 'a
09:02 larsrh err, what was it called again
09:04 larsrh !term sorted_list_of_set
09:04 isabelle-bot larsrh: sorted_list_of_set :: 'a set ? 'a list
09:04 larsrh there you go
09:04 larsrh the functions set and sorted_list_of_set are inverses
09:04 larsrh so you can keep a set and if you need it ordered you can convert it to a list
09:07 chindy ah, i see
09:09 int-e !term sorted_list_of_multiset
09:09 isabelle-bot int-e: sorted_list_of_multiset :: 'a
09:55 larsrh ~~/src/HOL/Library/Multiset is not included in isabelle-bot :-)
10:10 int-e !term CONST sorted_list_of_multiset
10:10 isabelle-bot int-e: Could not read term
10:10 int-e !term "CONST sorted_list_of_multiset"
10:10 isabelle-bot int-e: Could not read term
10:11 int-e !term CONST sorted_list_of_set
10:11 isabelle-bot int-e: sorted_list_of_set :: 'a set ? 'a list
10:11 int-e ah, it's just an uninformative error message, fair enough.
11:23 JCaesar int needs 'a :; ord though, no?
11:24 JCaesar And 'a :: linorder for most of the lemmas, or something?
11:25 int-e It's not entirely clear what an "ordered set" is; computer scientists and mathematicians will interpret those words in different ways, I think.
11:28 JCaesar for computer scientists, sets are mostly finite anyway, no?
11:38 int-e maybe I should say "programmer", in which case they become an unorderd container type.
11:39 larsrh or an interface for concrete implementations like "LinkedHashSet" :-)
11:58 dmiles joined #isabelle
12:31 silver joined #isabelle