Re: [isabelle] Trouble with the Int Theory



Thanks everyone! I think the error was actually easier to see with 

declare [[show_types]]

as I was working with 32 words. Clearly it is not the case that

of_int x = (0 :: 32 word) ==> x = 0

> On Nov 1, 2014, at 6:58 AM, Lars Noschinski <noschinl at in.tum.de> wrote:
> 
> On 01.11.2014 10:21, Peter Lammich wrote:
>> Hi,
>> 
>> try 
>>      note [[ show_sorts]]
>>      thm of_int_eq_0_iff
>> 
>> here, you will see that the of_int_eq_0_iff lemma only works
>> if the right hand side is in the ring_char_0 typeclass. 
> 
> The same can also be seen without show_sorts by hovering over the
> variables in the lemma.
> 
>  -- Lars
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.