Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-04-22

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

All times shown according to UTC.

Time Nick Message
07:02 jo2891 joined #isabelle
08:41 ammbauer larsrh jo2891: apply-script-style-question: for example, I do apply(rule) which gives me 6 subgoals. So if the next apply(simp) solves the first of those six subgoals, it should be indented by 5 spaces, correct?
08:41 ammbauer And yes, I'll try to use "subgoal" as much as possible.
08:42 ammbauer and Isar of course.
08:42 jo2891 ammbauer: general rule: don't use apply style ;-) Otherwise, yes indent with one space per goal.
08:43 jo2891 For short proofs, i.e. a couple of lines I don't use the indented apply-style. But some people will disagree.
08:48 larsrh I never indent, at all
08:50 ammbauer larsrh: aha, so we have you to blame.
08:51 ammbauer so like this: http://downthetypehole.de/paste/AVC3hDRn
08:52 * ammbauer frantically rewrites all his isabelle code
08:56 chuchucorny ammbauer: apply(simp; fail)
09:08 ammbauer chuchucorny: hmmm, which should be superfluous if I'm using sugoal like this: http://downthetypehole.de/paste/RdnMbkWu
10:06 jo2891 yes, in this case ; fail is not necessary
10:17 fracting joined #isabelle
10:29 silver joined #isabelle
10:35 Damaki joined #isabelle
10:58 jo2891 joined #isabelle
11:09 fracting joined #isabelle
11:33 jo2891 joined #isabelle
12:14 fracting joined #isabelle
16:19 dmiles joined #isabelle
16:20 dmiles joined #isabelle
19:02 kini joined #isabelle
21:57 tangentstorm joined #isabelle

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