Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-02-18

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

All times shown according to UTC.

Time Nick Message
00:30 aneas JCaesar, thank you. I'll try that
00:30 JCaesar (but yeah, pruvisto is right, you shouldn't use products in the first place, if you can.)
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/
02:48 wagle joined #isabelle
08:13 ammbauer pruvisto: You should change you're name to isabellebot.
08:13 ammbauer *your
09:49 JCaesar I bet that would freak some people out. :)
09:59 pruvisto heh
10:00 pruvisto JCaesar: using "split: prod.splits" and "simp: case_prod_unfold" both work usually
10:00 pruvisto iirc split introduces new variables for the two components whereas split_prod_unfold just uses "fst" and "snd"
10:01 JCaesar Ah, I guess that makes the case_prod_unfold the smarter options for products.
10:01 JCaesar Didn't know that.
10:01 pruvisto not sure whether it's smarter
10:01 pruvisto I started using that instead of splits a few years ago and I don't remember why
10:01 pruvisto one problem with splitting rules is that they introduce a lot of new variables with system-generated names
10:02 pruvisto so if you have like 8 of those, it can become difficult to figure out where a specific variables comes from and what it means
10:02 pruvisto but lots of "fst" and "snd" can also be ugly
10:02 JCaesar Btw, what's the difference between induct and induction, btw?
10:02 pruvisto "induction" is essentially a non-canonical fork of "induct"
10:03 pruvisto i.e. "induction" is not Makarius-approved
10:03 pruvisto I forgot what the details were but I'm sure Makarius will explain it to you in great detail if you're interested ;)
10:03 pruvisto I pretty much always use "induction", because I like the name better. ^^
10:04 pruvisto re: products, we once talked about this at the chair and apparently everyone had a different way to deal with tuples in goals ^^
10:07 JCaesar Makarius. -.-
11:33 silver joined #isabelle
17:05 silver_ joined #isabelle

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