Bounded little-endian u32 reader; zero is a fail-closed sentinel.
595def nativePhysicalEmbeddedWord32At =
596 (lambda unrestricted input : Bytes .
597 (lambda unrestricted offset : Nat .
598 (eliminate
599 DataBytesWord32ExactDecodeResult
600 (lambda unrestricted current : (family DataBytesWord32ExactDecodeResult) . Nat)
601 (dataBytesDecodeWord32LEExact
602 (nativePhysicalEmbeddedSliceOrEmpty input offset (byte-to-nat (byte 4))))
603 (branch DataBytesWord32ExactlyDecoded value telemetry . (modelWord32ToNatural value))
604 (branch DataBytesWord32ExactDecodeFailed code telemetry . zero))))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.