Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-08-16

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

All times shown according to UTC.

Time Nick Message
01:32 relrod joined #isabelle
01:32 relrod joined #isabelle
01:33 keep_learning joined #isabelle
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:03 wagle joined #isabelle
05:02 dmiles joined #isabelle
10:00 dave24 joined #isabelle
11:20 JCaesar I wonder if I could abuse isabellectl to make decent isabelle ebuilds…
12:45 larsrh Why not?
12:48 chindy Is there a more canonical way of writing there exits a negative component, given an euclidean_space , than: ?e ? Basis. e ? y < 0 ?
12:52 int-e wouldn't that be  ¬(y ? 0)?
12:55 pruvisto int-e: I don't think any euclidean space has an order defined like that
12:55 pruvisto but in an ordered_euclidean_space, that should work
12:57 int-e fair enough
13:06 chindy pruvisto: in addition to the other 2 lemmas, one might consider adding this: http://downthetypehole.de/paste/ths1ANQR
13:08 pruvisto I don't know, that seems both very specific and very simple
13:09 pruvisto fyi you can prove that in one line with "by (subst eucl_le) (auto simp: not_le inner_commute)"
13:12 chindy pruvisto: thanks!
13:13 chindy pruvisto: yea maybe it is to specific and very simple. If that is a criterion for not adding something, then its probably better to not add it
13:13 pruvisto kind of
13:14 pruvisto if it's something that I cannot imagine being of great general use and also being provable in a single line if you do need it, I'm reluctant to add it to the library
13:48 int-e hmm,  foo[of t, unfolded bar[of t], for t]  would be nice (that is, separating the "of" and "for" of the foo[of xyzzy for x] syntax)
14:28 pruvisto argh Curry Club
14:29 pruvisto "Im Curry Club sind sie auch alle schwul. Alle stehen auf Typen."
14:30 * int-e grübelt
14:30 pruvisto oh
14:30 pruvisto crap
14:30 pruvisto wrong channel
14:30 pruvisto sorry about that
14:31 pruvisto (Curry Club is a local functional programming meetup)
14:31 pruvisto Well, could have been worst. This is not the most embarrasing thing I could have mis-channed.
14:34 int-e Well, great. Now I'm wondering how "Typ" acquired that particular meaning in german...
14:36 pruvisto This drop in productivity was brought to you by Curry Club Augsburg
14:36 int-e Well it wasn't much of a drop.
14:37 pruvisto I know what you mean. ^^
22:13 JCaesar Hm, Typ in German is somewhat synonymous with personality. I'd guess people were talking about types (of guys) and the meaning drifted, or so. pruvisto, you're the linguist, no?

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