Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-10-10

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

All times shown according to UTC.

Time Nick Message
01:47 ilbot3 joined #isabelle
01: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:30 dmiles joined #isabelle
08:50 larsrh_ joined #isabelle
12:23 silver joined #isabelle
12:26 silver joined #isabelle
18:31 JCaesar Say, if I have a non-constructor-pattern on the right sight of an inductive-rule… does that just give a broken induction rule, or can I still somehow salvage that. I've been staring at proofs for lemmas like "inductive_pred bla' ==> bla' = insert a bla ==> inductive_pred foobla" and I'm still not sure whether they're supposed to work and i'm just too stupid, or whether the rule is really broken…
18:43 larsrh it's supposed to work, yes

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