[CakeML-dev] large_int
Ramana Kumar
Ramana.Kumar at cl.cam.ac.uk
Sun Mar 5 05:48:42 UTC 2017
The comment next to the number here
val large_int = ``268435457:int`` (* 2**28-1 *)
https://github.com/CakeML/cakeml/blob/master/compiler/backend/bvl_to_bviScript.sml#L22
does not match. (2**28-1 = 268435455).
Which is correct?
Can this number be defined somewhere? And verified (connected to some
proof)? Would backend_common be preferable for the definition than
bvl_to_bvi?
More information about the Developers
mailing list