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:05 
chindy 
I am currently thinking about how to represent correspondences/set valued functions in Isabelle, and came up with this: http://downthetypehole.de/paste/BWLUAIqN 
02:06 
chindy 
are there any other/standard ways of representing them? I was also wondering which of the 3 on the bottom would be best 
06:45 
pruvisto 
chindy: I found that the best thing to do is to totalise things 
06:45 
pruvisto 
i.e. if you have a "correspondence" between 'a and 'b and some concept of a domain and codomain, you should actually require that that correspondence returns the empty set outside the domain 
06:46 
pruvisto 
otherwise you can have to functions that are equal on the domain, but not equal outside the domain and that's annoying 
06:46 
pruvisto 
also, "… ? UNIV" is superfluous because it's always true 
08:38 
chindy 
pruvisto: so you mean something like: http://downthetypehole.de/paste/dMGjAy8a 
08:39 
chindy 
i still wonder whether it makes a noticable difference if i call it a subset of 'b set or an element of 'a set set 
11:08 

dave24 joined #isabelle 
11:34 
pruvisto 
yes, like that 
11:34 
pruvisto 
I really don't understand what this "graph" is about 
15:36 

aindilis` joined #isabelle 
15:46 
chindy 
pruvisto: its like the graph of a function... but i was going to put it into a separate def anyways, i just had it in there, for testing some stuff 
15:48 
pruvisto 
but what's the point? 
16:07 
chindy 
seems like there are multiple people having trouble with remote_vampire 
18:04 
larsrh 
me too 
19:35 

juanbono joined #isabelle 
21:47 

tautologico joined #isabelle 
23:52 

chindy joined #isabelle 
23:54 

Merv joined #isabelle 
23:54 

edwardk joined #isabelle 
23:54 

kyagrd joined #isabelle 
23:55 

JCaesar joined #isabelle 
23:56 

ChanServ joined #isabelle 
23:56 

isabellebot joined #isabelle 
23:56 

lispy joined #isabelle 
23:56 

relrod joined #isabelle 
23:56 

kini joined #isabelle 
23:57 

ezyang joined #isabelle 
23:59 

JCaesar joined #isabelle 