Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-03-06

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

All times shown according to UTC.

Time Nick Message
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/
04:25 stoopkid joined #isabelle
06:51 pruvisto rollary: "odd" is just an abbreviation for "┬Čeven"
06:51 pruvisto so if you only need case distinction, that's the way to go
06:51 pruvisto proof (cases "even n")
06:51 pruvisto then you get two cases for even and not even, i.e. odd
06:52 pruvisto if you want to do induction, you need to prove an induction rule first
06:52 pruvisto or just do "normal" induction on n (with the default induction rule for natural numbers)
06:53 pruvisto and then a case distinction in the step
10:34 silver joined #isabelle
14:28 GK___1wm_SU joined #isabelle
22:10 silver joined #isabelle

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