Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-08-25

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

All times shown according to UTC.

Time Nick Message
01:51 ilbot3 joined #isabelle
01:51 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:43 aindilis joined #isabelle
08:34 aindilis joined #isabelle
12:33 chuchuco1ny joined #isabelle
12:33 int-e joined #isabelle
14:14 chindy the isabelle latex package has symbols that require \usepackage{amssymb} but does not load this package by itself, is this intentional ?
14:15 juanbono joined #isabelle
14:24 chuchuco1ny pruvisto: Hey Isabelle with IO programming can prove HelloWorld correct (with the appropriate assumptions): https://github.com/diekmann/Isabelle-Hello-World/blob/master/HelloWorld.thy#L63
14:27 pruvisto chuchuco1ny: that looks pretty inconsistent to me
14:32 chuchuco1ny pruvisto: why?
14:33 pruvisto oh wait
14:33 pruvisto yeah I misunderstood something at first
14:35 pruvisto I wonder if something like this could be integrated into Imperative HOL
14:36 chuchuco1ny I wonder if something like this could make it into the AFP as the simplest possible example for HelloWorld (for programmers) in Isabelle
14:37 chuchuco1ny I mean the main functions looks quite okay to me
15:31 chuchuco1ny pruvisto approved?
15:35 pruvisto I'm not sure. I think for this to be a good idea to have in the AFP, this should be "battle-tested"
15:35 pruvisto i.e. if this can be used reasonably well for something bigger than a Hello World, it might make sense to have a Hello World in the AFP using it
15:36 pruvisto but the mailing list, and in particular the AFP editors, will be more qualified to answer this than I.
17:00 tautologico joined #isabelle

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