Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-03-28

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

All times shown according to UTC.

Time Nick Message
01:32 ezyang joined #isabelle
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/
02:44 wagle joined #isabelle
05:51 pruvisto JCaesar: I think elim is essentially an "eager erule"
05:51 pruvisto and it ignores chained facts
05:51 pruvisto bit like intro vs. rule
05:52 pruvisto I'm not 100% sure, but that's how I use it
05:52 pruvisto chindy: because someone asked a question about vectors on StackOverflow just a few hours ago
05:53 pruvisto otoh, I do vaguely remember that you already knew about them before today, so in retrospect, I could have known it probably wasn't you
05:53 pruvisto anyway, I was just wondering
05:54 pruvisto What you ought to write is "thus False proof (rule disjE)"
05:54 pruvisto you didn't actually give the disjunction (i.e. the fact that "foo ∨ bar") to disjE, so after you've proven the two cases, you're still left with the disjunction as a goal
05:55 pruvisto More idiomatically, you can just write thus False proof
05:55 pruvisto because disjE is the default rule for these situations anyway
07:29 JCaesar pruvisto: Yes, @ eager rule. But one of them has the additional effect of apply -, the other doesn't (and won't work if there's 'using'-facts).
07:31 pruvisto that's what I said – it ignores chained facts
07:31 pruvisto well, okay, it adds them to premises
07:31 pruvisto like every SIMPLE_METHOD
07:33 larsrh erule is somewhat strange wrt chained facts
07:33 larsrh it works entirely unlike everything else
07:42 chindy ah thanks  JCaesarhow would you do proof cases ?
07:42 pruvisto proof (cases rule: disjE) should work
07:42 pruvisto you have to chain in the disjucntion, of course
07:43 pruvisto "cases" is, I guess, the "proper Isar way" to apply elimination rules
07:43 pruvisto it has the advantage of assigning proper names to the different cases
07:44 pruvisto but only when the rule that is used /has/ such names assigned
07:53 JCaesar chindy: I don't think you even need to specify the rule for cases. just applying it without any parameters might be enough…
08:07 pruvisto JCaesar: I think I tried that yesterday and it did something different
08:07 pruvisto but I would have expected it to work as well
11:00 silver joined #isabelle
18:12 ertesx joined #isabelle

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