HomeIsabelle/Phabricator

Fix IntInf.log2 on big-endian with GMP. It assumed that long format arbitrary…

Description

Fix IntInf.log2 on big-endian with GMP. It assumed that long format arbitrary precision numbers were always little-endian. Also improve
IntInf.andb, IntInf.orb and IntInf.xorb when one or both arguments are short.

Details

Provenance
dcjmAuthored on Oct 26 2023, 7:18 PM
Parents
rPOLYMLb6fc915c9000: Tweak heap sizing to deal better with allocating a large array in a small heap.
Branches
Unknown
Tags
Unknown