[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