Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-04-27

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
00:06 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/
03:25 hazyPurple joined #isabelle
03:42 hazyPurple joined #isabelle
07:26 hazyPurple joined #isabelle
08:00 dave24 joined #isabelle
08:02 hazyPurple joined #isabelle
08:26 ertes joined #isabelle
10:55 ertes joined #isabelle
12:18 ertes joined #isabelle
12:31 ertes joined #isabelle
12:36 larsrh Why do I need to build all of HOL-Library now to use HOL-Probability?
12:46 int-e . o O ( because we need more people using the 64 bit version of Isabelle )
12:46 pruvisto larsrh: since when do you use HOL-Probability
12:47 pruvisto I thought you avoided numbers at all cost
12:50 larsrh my session failed, I wanted to inspect that
12:51 larsrh but Larry has apparently already fixed it
13:24 JCaesar Yeah, inventing numbers was a bad idea.
13:43 int-e natural numbers are all right
13:44 larsrh everything else is terrible
14:32 ertes joined #isabelle
14:41 JCaesar Natural numbers are the worst. They lure you in and then, you're trapped.
15:36 pruvisto real numbers at least have nice properties
15:36 pruvisto complex numbers have even nicer properties
15:36 pruvisto natural numbers are so… chunky
18:38 larsrh_ joined #isabelle
22:14 lispy joined #isabelle
22:19 ertes joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary