Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-12-09

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

All times shown according to UTC.

Time Nick Message
00:59 dmiles joined #isabelle
02:48 ilbot3 joined #isabelle
02: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/
05:29 dmiles joined #isabelle
09:25 dmiles joined #isabelle
10:31 JCaesar https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-December/007252.html so what is the tale that you should be telling?
10:31 JCaesar (someone mind bouncing me that e-Mail, so I can reply to it on the isabelle mailing list?)
10:55 larsrh JCaesar: bounced
10:56 JCaesar ty
10:56 larsrh The answer to your question is, to be frank, "who the heck knows?"
10:56 larsrh It is pretty much obvious to anyone except for one person that this is a critical issue that needs to be addressed
11:04 JCaesar :D
11:30 silver joined #isabelle
11:35 JCaesar Heh, I found a case where the "proof outline with cases" (at least that one from 2016-1-RC2 is wrong).
11:36 JCaesar make yourself a lemma two_list_induct_somethingsomething[case_names Nil Cons]: "P [] [] ==> (!! a S T. P S T ==> P (a # S) T &&& P S (a # T)) ==> P S T", and then try using that in some proof(induction S T rule: two_list_induct)
11:37 JCaesar (anyway, how do I work with subcases?)
11:37 JCaesar (Oh. Just use the case statement twice.)
13:08 larsrh JCaesar: that is a known limitation
13:08 JCaesar kk
16:15 ammbauer joined #isabelle
18:14 dmiles joined #isabelle
19:37 silver joined #isabelle
22:44 silver_ joined #isabelle

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