Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-06-03

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

All times shown according to UTC.

Time Nick Message
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:01 fracting joined #isabelle
03:32 fracting joined #isabelle
06:11 fracting joined #isabelle
07:15 fracting joined #isabelle
08:37 kyagrd_ joined #isabelle
08:39 cocreature joined #isabelle
08:43 int-e joined #isabelle
09:51 silver joined #isabelle
10:56 silver_ joined #isabelle
13:26 fracting joined #isabelle
14:43 jo2891 joined #isabelle
15:04 fracting joined #isabelle
18:58 fracting joined #isabelle
20:12 cocreature I keep running into cases that I can solve using "erule somecasesrule" followed by "auto" but not by "auto elim:somecasesrule". am I simply “unlucky” or is elim the wrong thing to use here?
20:14 larsrh how about "auto elim!:"?
20:16 cocreature larsrh: that seems to result in a timeout rather than the “failed to apply proof method” I’m getting without the !
20:17 larsrh I don't know for sure exactly, but I think cases rules are not usually supposed to be used as elim rules
20:17 larsrh so the other think I can suggest would be to use (cases rule: somecasesrule, auto)
20:18 larsrh *thing
20:18 cocreature ah yeah that’s nicer than erule
21:30 chuchucorny why is cases nicer than erule?
21:32 chuchucorny (I use apply(erule foo, othermethod) excessively ;-))
21:34 larsrh chuchucorny: depends on the kind of rule :-)
21:52 jo2891 joined #isabelle

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