Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-04-01

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

All times shown according to UTC.

Time Nick Message
00:43 Damaki joined #isabelle
02:58 andromeda-galaxy joined #isabelle
07:34 fracting joined #isabelle
07:52 fracting joined #isabelle
11:36 fracting joined #isabelle
11:39 fracting joined #isabelle
11:47 Damaki joined #isabelle
12:22 dmiles joined #isabelle
12:27 chuchucorny why can't I define a function when I'm doing an instantiation?
12:27 larsrh chuchucorny: I think you can
12:27 larsrh Do you get any error message?
12:28 chuchucorny in an instantiation context for linorder, I'm defining function (sequential) less_eq_iface ...
12:28 chuchucorny when I try "termination less_eq_iface" I get the error message "Not a function: "less_eq_iface""
12:28 larsrh OK, let me check ...
12:31 larsrh Try this: termination "less_eq :: iface => _ => bool"
12:31 larsrh Although I'll readily admit that this is annoying
12:40 chuchucorny thanks, works (but is ugly)

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