Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-06-27

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

All times shown according to UTC.

Time Nick Message
01:51 ilbot3 joined #isabelle
01:51 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:13 mal``` joined #isabelle
05:43 lispy joined #isabelle
10:29 larsrh joined #isabelle
10:30 silver joined #isabelle
12:27 ilbot3 joined #isabelle
12:27 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/
12:47 ilbot3 joined #isabelle
12: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/
13:09 ilbot3 joined #isabelle
13:09 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/
13:43 ilbot3 joined #isabelle
13:43 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/
14:19 ilbot3 joined #isabelle
14:19 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/
14:52 ilbot3 joined #isabelle
14:52 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/
15:24 ilbot3 joined #isabelle
15:24 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/
15:46 ilbot3 joined #isabelle
15:46 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/
15:55 ilbot3 joined #isabelle
15:55 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/
16:15 ilbot3 joined #isabelle
16:15 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/
16:20 ammbauer what rule do I have to add to auto, if I have something like "case xs of [] => P | x#xs' => Q" in my assumptions and I want it to case split automatically?
16:26 larsrh split: list.splits
16:27 ammbauer huh, okay. now it's working ;shrug
22:03 qwertyyyy joined #isabelle
23:42 qwertyyyy what does it mean when I use quickcheck on a lemma and for P in a expression like P x it finds a counterexample "{}" or something similar
23:42 qwertyyyy for example :
23:42 qwertyyyy "(P z) ⟹ ( P y )"
23:43 qwertyyyy quickcheck finds : P  = {a_1} ;  z = a_1 ; y = a_2
23:44 qwertyyyy I understand why it is wrong ... I just don't understand what quickcheck wants me to tell by "P = {a_1}"

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