Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-11-29

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

All times shown according to UTC.

Time Nick Message
00:50 chuchucorny joined #isabelle
00:50 ammbauer joined #isabelle
02:47 ilbot3 joined #isabelle
02:47 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/
05:28 chuchucorny joined #isabelle
10:15 chuchucorny joined #isabelle
11:19 silver joined #isabelle
13:09 JCaesar btw, ThreeOfEight, you recommended NO_MATCH to me a while ago…
13:09 ThreeOfEight Yes.
13:10 JCaesar Hm, it's not easy to use…
13:10 ThreeOfEight Can you be more specific?
13:10 ThreeOfEight What do you want to achieve?
13:10 JCaesar http://downthetypehole.de/paste/UuHCVlnW
13:10 JCaesar But I just noticed where I'm going wrong…
13:11 ThreeOfEight When NO_MATCH doesn't work, try reversing the arguments
13:11 ThreeOfEight I can never remember which way round they have to be
13:12 JCaesar well, in the cases where I got it to work, it's quite powerful.
13:14 ThreeOfEight so does it work now?
13:15 ThreeOfEight What are you doing there? Natural deduction?
17:23 silver joined #isabelle
21:03 JCaesar Sequent calculus, actually. And yeah, I've mostly got it working…

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