Re: [isabelle] Trouble with the Int Theory
Thanks everyone! I think the error was actually easier to see with
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:
>> 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