Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-03-15

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

All times shown according to UTC.

Time Nick Message
06:56 pruvisto JCaesar chindy: I'd say if there's a relatively obvious one-line proof (i.e. not metis plus several facts), that is the best way to go
06:57 pruvisto both because it avoids going into unnecessary detail and because it is probably the most robust solution
06:57 pruvisto but once the only thing that works is metis plus 20 different facts, or a 10-step apply script, you should better write an Isar proof
06:57 pruvisto It will be more readable, more robust, more maintainable, and faster
06:58 pruvisto (because at every "by", proof checking can be forked to the background, so an Isar proof with 5 "by"s will usually process faster than an apply script with 5 "apply"s
09:46 silver joined #isabelle
12:23 ammbauer joined #isabelle
13:19 silver joined #isabelle
22:12 silver_ joined #isabelle
22:26 ammbauer joined #isabelle

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