Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-07-03

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

All times shown according to UTC.

Time Nick Message
03:40 qwertyyyy pruvisto: oh ... I see it now ... thank you :)
04:00 keep_learning joined #isabelle
06:01 pruvisto chindy: well, every type class does define a locale
06:03 pruvisto for instance, the "linorder" class has the locale "class.linorder"
06:03 pruvisto you can use that like any other locale
06:04 pruvisto but you might run into some problems in practice; this is not something that people do very often in practice
07:59 silver joined #isabelle
08:16 silver_ joined #isabelle
08:27 int-e . o O ( I'm worried to see what Makarius calls "relatively lightweight" )
08:37 pruvisto haha
08:38 pruvisto well, electrons are relatively lightweight :P
08:42 larsrh "lightweight" is a meaningless term
08:42 larsrh Makarius, of all people, should be refusing to use it
08:43 int-e please point that out on the mailing list. you start with "just like 'bug'"...
08:43 larsrh no, quite the opposite, in fact
08:43 larsrh "Just like Jenkins, this is lightweight ..."
08:44 pruvisto I'm going to use this defence the next time my nan tells me I'm getting fat
08:44 pruvisto "Well, you see, 'lightweight' is a meaningless word…"
08:44 larsrh do it in English though
08:45 pruvisto I doubt her English will suffice
08:45 pruvisto Her English vocabulary is limited to things you could shout after passing American soldiers in post-war Munich and expect to get chocolate in return.
08:46 pruvisto So, mostly the word ‘chocolate’
08:48 int-e pruvisto: "I may not be lightweight, but I'm relatively lightweight"?!
08:49 pruvisto haha
09:19 chindy pruvisto: thing is i want to prove some things given a preorder where 'a is of type ordered_euclidean_space, preoders is a class though
09:20 pruvisto um, ordered_euclidean_space is already a subclass of "order"
09:20 pruvisto so that entails preorder
09:22 larsrh !term x::'a::{preorder,ordered_euclidean_space}
09:22 isabelle-bot larsrh: Could not read term
09:23 larsrh ah, that's in HOL-Analysis
21:10 silver joined #isabelle

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