Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2015-11-04

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

All times shown according to UTC.

Time Nick Message
02:48 ilbot3 joined #isabelle
02:48 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/
07:30 mal`` joined #isabelle
15:31 mal`` joined #isabelle
15:33 mal`` joined #isabelle
17:05 tautologico I can't seem to find "datatype" in the reference manual
20:33 ThreeOfEight tautologico: it probably isn't in the reference manual
20:34 ThreeOfEight because it isn't a part of Isabelle/Isar
20:34 ThreeOfEight it's basically a "userspace" library
20:34 ThreeOfEight there's a datatype manual on the Isabelle website
21:00 tautologico isn't it defined by HOL?
21:01 tautologico I mean, in the HOL object logic
21:02 tautologico the HOL chapters in the manual mention datatypes but the links to it (e.g. from the definition of primrec) are broken
21:03 tautologico I'll check the tutorial on datatypes
21:15 ThreeOfEight the Isabelle/Isar reference manual has nothing to do with HOL
21:15 tautologico btw, if fun is more general, why use primrec?
21:15 ThreeOfEight actually, that's wrong
21:16 ThreeOfEight there are some HOL-specific things in the reference manual
21:16 ThreeOfEight even old-style datatypes
21:16 tautologico yes, part III of the manual
21:16 tautologico that's what I was referring to
21:16 ThreeOfEight as for primrec: it's faster and generates fewer specialised theorems
21:16 ThreeOfEight (which you probably don't need anyway in most cases if the function is primitively recursive)
21:18 ThreeOfEight also, there are some cases like trees with infinitely many subtrees per node, where primrec will work fine but fun might not be able to prove termination automatically
21:18 ThreeOfEight there was a question about that on Stack Overflow a while ago
21:18 ThreeOfEight but if you want to know anything about datatypes, you should read this: http://isabelle.in.tum.de/dist/Isabelle2015/doc/datatypes.pdf
21:21 tautologico I'm reading it right now
21:21 tautologico thanks
21:22 ThreeOfEight there might be something in some PhD thesis as well
21:22 ThreeOfEight and there are probably a number of papers on the topic as well
21:22 ThreeOfEight but I think the important stuff should all be in that PDF as well
21:22 tautologico yes, the tutorial has reference on the papers
21:23 ThreeOfEight if you have specific questions, you can also always ask them on Stack Overflow or on the mailing list
21:23 ThreeOfEight (or here, but the people who are most likely to be able to answer them are not here, I think)
21:23 tautologico I usually think my questions are still too basic for the mailing list
21:24 ThreeOfEight well, if you really think so, you can ask here, I guess
21:24 ThreeOfEight if you can't find the answer in the tutorial and I don't know it either, I'd say it's not too basic for the mailing list

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