IRC log for #isabelle, 2017-08-14

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: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 isabelle-bot 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