# IRC log for #isabelle, 2016-04-14

All times shown according to UTC.

Time Nick Message
04:28 dmiles_afk joined #isabelle
04:29 dmiles_afk joined #isabelle
04:29 dmiles_afk joined #isabelle
04:30 dmiles_afk joined #isabelle
04:30 dmiles_afk joined #isabelle
04:31 dmiles joined #isabelle
04:32 dmiles joined #isabelle
04:39 kini joined #isabelle
06:03 larsrh_ joined #isabelle
06:03 larsrh_ joined #isabelle
11:00 fracting joined #isabelle
11:37 Damaki joined #isabelle
12:09 Damaki_ joined #isabelle
12:17 fracting joined #isabelle
13:00 dmiles joined #isabelle
13:53 kini joined #isabelle
13:53 fracting joined #isabelle
17:25 larsrh left #isabelle
17:27 fracting joined #isabelle
17:37 larsrh joined #isabelle
19:45 larsrh joined #isabelle
20:17 JCaesar What kind of type is "42"? why is definition "answer == undefined :: 42" valid?
20:18 larsrh it's a numeral type
20:19 JCaesar what are its members?
20:19 larsrh the thing you use for words
20:19 larsrh e.g. "32 word"
20:19 larsrh JCaesar: numbers from 0 to n - 1
20:19 larsrh err
20:19 larsrh 2^n - 1
20:20 larsrh no
20:20 larsrh I'm confusing myself
20:21 larsrh Here's the definition: http://isabelle.in.tum.de/repos/isabelle/file/38906f0e4633/src/HOL/Library/Numeral_Type.thy
20:21 JCaesar lemma "2 ∈ {a :: 42 |a. True}" does seem to be true…
20:21 JCaesar Ah…
20:21 larsrh lemma "CARD(17) = 17" by simp
20:21 larsrh lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp
20:21 larsrh So it's members are 0 ... n - 1
20:22 Damaki_ joined #isabelle
20:22 larsrh The members of n word are 0 ... 2^n - 1
20:24 JCaesar That's pretty cool. Let's see if I happen to come across an application of that.
21:54 lispy joined #isabelle
22:04 fracting joined #isabelle
23:34 Damaki joined #isabelle