Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-08-16

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

All times shown according to UTC.

Time Nick Message
09:00 silver joined #isabelle
10:03 dmiles joined #isabelle
10:53 Damaki joined #isabelle
11:45 dmiles joined #isabelle
12:36 Damaki joined #isabelle
12:38 JCaesar Btw, is it possible to do something like definition "foo (w::('l::len) word) = (case TYPE('l) of TYPE(32) => … | …)"
12:39 JCaesar (It's not really useful to me, I'm just curious.)
13:22 ThreeOfEight …that sounds like a type error
13:22 ThreeOfEight TYPE('l) should be of type "'l itself"
13:22 ThreeOfEight while TYPE(32) is of type "32 itself"
13:23 ThreeOfEight if 'l has the sort "typerep", you could do a comparison on the type representation
13:23 ThreeOfEight but that would be pretty horrible
13:24 ThreeOfEight a perhaps better possibility would be to retrieve an actual natural number from the length type parameter
13:24 ThreeOfEight i.e. the actual natural number "32" from the type "32"
13:24 ThreeOfEight (e.g. with CARD('l), I think)
13:24 ThreeOfEight then you could do "if CARD('l) = 32 then … else …"
16:08 Damaki joined #isabelle
19:43 Damaki joined #isabelle

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