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 
isabellebot 
larsrh: ordered_set_of_list :: 'a 
09:01 
larsrh 
!term ordered_list_of_set 
09:01 
isabellebot 
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 
isabellebot 
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 
inte 
!term sorted_list_of_multiset 
09:09 
isabellebot 
inte: sorted_list_of_multiset :: 'a 
09:55 
larsrh 
~~/src/HOL/Library/Multiset is not included in isabellebot :) 
10:10 
inte 
!term CONST sorted_list_of_multiset 
10:10 
isabellebot 
inte: Could not read term 
10:10 
inte 
!term "CONST sorted_list_of_multiset" 
10:10 
isabellebot 
inte: Could not read term 
10:11 
inte 
!term CONST sorted_list_of_set 
10:11 
isabellebot 
inte: sorted_list_of_set :: 'a set ? 'a list 
10:11 
inte 
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 
inte 
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 
inte 
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 