# IRC log for #isabelle, 2017-06-06

All times shown according to UTC.

Time Nick Message
01:18 ertes joined #isabelle
01:48 ilbot3 joined #isabelle
01:48 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/
06:17 ammbauer is there a way to find the corresponding term to a symbol? for example I have this expression "(λB. ∫⇧+ M'. emeasure M' B ∂M)". How do I find out what ∫⇧+ or ∂ stand for?
06:44 pruvisto I usually just do "ML ‹@{term "foo"}›"
06:45 pruvisto or you can ask your friendly advisor and he'll tell you that "∫⇧+" and "∂" are both part of the syntax for nn_integral :P
06:47 pruvisto the thing after the ∂ is the measure space that you integrate "over"
06:47 pruvisto i.e. in the "normal" integral that's usually "lborel", the Lebesgue–Borel measure
06:47 pruvisto if you choose "count_space A", your integral just corresponds to the sum over all elements in the set A
06:47 pruvisto nn_integral has the added twist that it "ignores" the negative part of the function
06:47 pruvisto so "nn_integral f M" is essentially the integral of "max(f, 0)" over the entire space of M
06:47 pruvisto (The advantage of nn_integral is that it always exists as long as f is measurable, though it may be infinite)
06:57 ammbauer pruvisto: thanks
06:57 ammbauer it would be really cool if you could also click on the symbols and jump to the definition
07:29 pootler joined #isabelle
07:31 pruvisto ammbauer: uuh, i think you can
07:34 Merv_ left #isabelle
07:35 Merv_ joined #isabelle
07:36 Merv_ left #isabelle
07:43 ammbauer pruvisto: not with translations like ∫⇧+. pressing Ctrl and hovering over it does nothing.
07:44 pruvisto I think "syntax" is the better word here
07:44 pruvisto "translation" is just the stuff that maps the syntax to actual terms
07:46 pruvisto hm indeed
07:46 pruvisto that is unfortunate
07:46 pruvisto maybe you could ask on the mailing list
07:46 pruvisto in my naïvete, I think this shouldn't be too hard
07:46 pruvisto all the information should be there
08:59 silver joined #isabelle
09:38 larsrh I am sorry to inform you that pruvisto is at it again
09:38 larsrh 22nd AFP entry
10:17 int-e soon there'll be enough to fill an Advent calendar
10:18 larsrh there are currently (including devel) 361 AFP entries
10:19 larsrh so soon there'll be enough to fill a calender :-)
11:13 stoopkid joined #isabelle
11:58 pruvisto I have some more in my pipeline
11:58 pruvisto at least 3
11:58 pruvisto Maybe once I have 25 AFP entries I should buy some cake or something to celebrate
12:30 larsrh no, you should buy a new server
12:57 JCaesar