1425def stdU32ToU16 =
1426 (lambda unrestricted value : (family ModelWord32) .
1427 (eliminate
1428 ModelWord32
1429 (lambda unrestricted current : (family ModelWord32) . (family StdU16))
1430 value
1431 (branch ModelWord32Value b0 b1 b2 b3 . (stdU16FromBytes b0 b1))))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.