Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-05-24

| 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/
02:03 fracting joined #isabelle
02:26 fracting joined #isabelle
04:31 fracting joined #isabelle
05:00 fracting joined #isabelle
06:18 kyagrd joined #isabelle
11:04 fracting joined #isabelle
11:37 fracting joined #isabelle
12:03 fracting joined #isabelle
12:39 fracting joined #isabelle
13:36 silver joined #isabelle
18:33 chuchucorny I just heared there is a quickcheck (as in haskell quickcheck) for ML. Is this available in Isabelle/ML?
19:54 larsrh it's called Spec_Check
19:55 larsrh you can find it in the distribution
19:56 cocreature is there a way to refer to the induction hypothesis when my cases don’t have names? I’m doing induction using the induction rule of a fun and the hypothesis is fairly long so I’d like to avoid having to type the whole thing
19:59 int-e if you have case (1 x y), then the 1 is a case name and you can refer to the induction hypothesis as 1.
19:59 int-e (in my experience)
19:59 cocreature int-e: ah great that works! I was trying 1.IH like Case.IH and that doesn’t do the trick
20:05 int-e cocreature: oh. you need quotes for that... "1.IH" works.
20:05 cocreature int-e: ah I tried "1".IH :)
23:47 fracting joined #isabelle

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