Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2015-11-17

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

All times shown according to UTC.

Time Nick Message
03:32 rofer joined #isabelle
04:56 ThreeOfE1ght joined #isabelle
04:56 int-e_ joined #isabelle
04:58 mbrcknl_ joined #isabelle
05:02 mal`` joined #isabelle
05:26 ThreeOfEight joined #isabelle
11:28 dmiles_afk joined #isabelle
19:47 barrucadu I'm having some difficulty, I've got a recursive data type and a function, and don't really know how to approach the termination proof
19:47 barrucadu Here's a minimal example: https://gist.github.com/barrucadu/b5fc0b3f440b354cca34
22:16 ThreeOfEight barrucadu: if you stick around i'll look at it tomorrow morning
22:19 ThreeOfEight i.e. in ten hours or so
23:02 int-e barrucadu: if you use pattern matching on the left-hand side instead of a 'case' it works automatically. (in fact it becomes primitive recursive that way)
23:02 int-e err
23:03 int-e sorry for that, I tested wrong
23:04 int-e (I made a copy of the function and didn't change the recursive call... unsurprisingly that worked)

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