[Agda] Are .agdai files portable?

[Nils Anders Danielsson]

On 2010-04-12 15:38, Nils Anders Danielsson wrote:
> I see that interface files contain Ints and Doubles, which are not
> guaranteed to have a certain size or format. Data.Binary stores Ints
> using 64 bits on both 32-bit and 64-bit platforms, but truncates the
> values when reading on 32-bit platforms. I have now replaced uses of
> Int with Int32 (I hope this does not incur a performance penalty on
> 64-bit platforms); is there a platform-independent variant of Double?

By the way, the potential problems with Doubles are irrelevant for the
standard library, which does not use them. (Doubles are only stored in
interface files if you use BUILTIN FLOAT.)

--
/NAD