Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-11-06

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

All times shown according to UTC.

Time Nick Message
00:05 JCaesar heh, and in case you fix up m: in that lemma (by adding a ~~ in front of the mask 31), you can trigger a z3 and cvc4 error if you sledgehammer on u:…
00:47 larsrh trying it out at the moment
00:48 larsrh there's a broken import in Routing_Table
00:59 larsrh ok, the problem is the "is" match
00:59 larsrh if you change that to (is "∃x. _ ∧ (∀p. ?t2 x p)") it works
01:00 larsrh error message is a bit confusing though
09:48 JCaesar indeed…
09:49 JCaesar ty
10:02 JCaesar now, it doesn't feel like it's the first time I ran into this…

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