[isabelle-dev] [isabelle] bit vs. bool in HOL-Word
florian.haftmann at informatik.tu-muenchen.de
Thu Dec 12 16:21:39 CET 2013
>> * Concerning Bit.thy – this is something separate, a formalisation of
>> the Z2 field actually. It stand aparat, and references of the Word
>> theories to bit should be replaced by bool.
>> * Concerning bit operations – these should use bool uniformly. Both
>> explicit list conversions and implicit structural operation like
>> test_bit and set_bit are relevant for user space. _ BIT _ is a historic
>> accident. The idea is to clearly separate the bit operations into
>> separate HOL-Library theories, to make them properly available for
>> applications which do not need words but bits.
> See now
> where bool replaces bit as digit type throughout.
> I invite users with heavy applications of the Word library to check this
> first before bringing it upstream.
Shall I assume that the silence on this thread means that everybody is
fine with pushing this matter?
If silence continues beyond Dec 21st, I will interpret this as »Go!«.
Otherwise just give me a shout.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 263 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev