336def modelWord32ToNatural =
337 (lambda unrestricted value : (family ModelWord32) .
338 (eliminate
339 ModelWord32
340 (lambda unrestricted current : (family ModelWord32) . Nat)
341 value
342 (branch
343 ModelWord32Value
344 b0
345 b1
346 b2
347 b3
348 .
349 (naturalAdd
350 (byte-to-nat b0)
351 (naturalMultiply
352 byteNaturalTwoHundredFiftySix
353 (naturalAdd
354 (byte-to-nat b1)
355 (naturalMultiply
356 byteNaturalTwoHundredFiftySix
357 (naturalAdd
358 (byte-to-nat b2)
359 (naturalMultiply byteNaturalTwoHundredFiftySix (byte-to-nat b3))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.