Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-09-06

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

All times shown according to UTC.

Time Nick Message
00:32 aindilis joined #isabelle
00:52 Warrigal_ Yo.
00:52 Warrigal_ So Isabelle/Pure is the base system, right? Everything starts from there?
00:55 Warrigal_ I'd like to jump right in and start writing Isabelle/Pure, skipping Isabelle/HOL... but it's not obvious how I can learn how Isabelle/Pure works.
00:55 Warrigal_ I found something that pointed me at this, and it looks like it may be a good example to imitate: https://github.com/seL4/isabelle/blob/master/src/HOL/Isar_Examples/Higher_Order_Logic.thy
00:55 Warrigal_ But I haven't been able to find information about, say, what "class" means.
01:26 Warrigal_ joined #isabelle
01:30 Warrigal_ Can I... pretty much just declare whatever inference rules I want?
01:36 Warrigal_ What I'd like to say, perhaps, is that there's a thing called "flimcat", and that "flimcat" has the type "fp flimcat"... except it looks like maybe the head of a parameterized type is written on the right, in which case the type would be "flimcat fp".
01:36 Warrigal_ I'm not sure if you can declare something as having a type and then later declare it as additionally having a different type.
01:38 Warrigal_ Or whether each term must have exactly one type, no more and no less.
01:50 Warrigal_ Whelp, I guess I'll take another look at things later...
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/
03:29 JCaesar qertyyyy: A lot of proofs seem to do 'finally show ?thesis ..' or 'finally show thesis .' depending on what you want, those might be your friends. (.. is equal to 'by rule', iirc, so it will apply refl if available. '.' is just by assumption, or so…)
05:29 ilbot3 joined #isabelle
05:29 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/
14:42 ilbot3 joined #isabelle
14:42 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/
14:48 ilbot3 joined #isabelle
14: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/
15:16 juanbono joined #isabelle
21:29 Warrigal_ joined #isabelle
21:43 Warriga_l joined #isabelle
23:47 Warrigal_ joined #isabelle

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