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 