Time 
Nick 
Message 
10:37 

isabellebot joined #isabelle 
10:41 
larsrh 
now with timeout and truncation 
10:43 
inte 
off with their heads! 
10:43 
inte 
!value 20 * 20 :: nat 
10:43 
isabellebot 
inte: Failed, probably timeout? 
10:43 
inte 
(but I expect it chops off tails) 
10:43 
inte 
!value 20 * 2 :: nat 
10:44 
isabellebot 
inte: Failed, probably timeout? 
10:44 
inte 
!value 2 * 2 :: nat 
10:44 
isabellebot 
inte: Failed, probably timeout? 
10:44 
inte 
well at least the timeout works! 
10:46 
larsrh 
heh 
10:46 
larsrh 
I didn't say the timeout was particularly large :p 
10:47 

isabellebot joined #isabelle 
10:47 
larsrh 
in all seriousness though, this wasn't as intended 
10:47 
larsrh 
!value 20 * 2 :: nat 
10:47 
isabellebot 
larsrh: Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc ( 
10:47 
inte 
I assumed as much. 
10:47 
pruvisto 
I should finally fix printing of nat 
10:47 
pruvisto 
before the next release 
10:47 
inte 
But it was funny. :) 
10:47 
larsrh 
inte: it looks like Isabelle ignored my humble request to interrupt the thread 
10:48 
* larsrh 
gets out the pitchfork 
10:48 
inte 
. o O ( !import Code_Target_Nat ) 
10:50 
larsrh 
oh well, that's for another hacking session :) 
10:51 
larsrh 
for now I blame PircBotX 
14:32 

ilbot3 joined #isabelle 
14:32 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
14:34 

ilbot3 joined #isabelle 
14:34 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
16:48 

mal`` joined #isabelle 
19:31 
qwertyyyy 
hi , why is "(⋀y .y = B ⟹ A) ⟹ A" true but "⋀y. (y = B ⟹ A) ⟹ A" not ? 
21:06 
pruvisto 
qwertyyyy: well, the second one means "∀y. ((y = B → A) → A)" 
21:07 
pruvisto 
and that is, in general, false, if one chooses some y ≠ B 
21:08 
pruvisto 
the first one means "(∀y. (y = b → A)) → A", which is true, since one can simply instantiate y = B. 
21:08 

keep_learning joined #isabelle 
22:04 
chindy 
What if in this case http://downthetypehole.de/paste/Hg7Q66YW (shown by inte) A is not a locale but a typeclass how would that work ? 