From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hello all,
in HOL-Word, there are two competing formalisations of ints as bit strings:
Bit_Representation.thy with an implicit representation using
constructors and destructors etc. (on using bit instead of bool see my
previous mail);
Bool_List_Representation.thy with an explicit representation as list
of bools.
Currently, they stand side by side. But one could be more easily
developed in terms of the other.
For this, it is helpful to know which of there (both, one, none) are
actually used in existing applications.
Thanks for any hint,
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC