AlphaGitHub
Source/Packages

Data.Bytes

packages/foundation/standard/src/Data/Bytes.alpha

1,462 lines172 declarations57.0 KiBSHA-256 55edb6a9adcd
Download exact fileView at revisionf5034773ad4bb52133

def · lines 1120–1138

dataBytesReadWord32LE

Full file
1120def dataBytesReadWord32LE =
1121  (lambda unrestricted input : Bytes .
1122    (nat-eliminate
1123      (lambda unrestricted current : Nat . (family DataBytesWord32DecodeResult))
1124      dataBytesWord32Failure
1125      (lambda unrestricted fitsPredecessor : Nat .
1126        (lambda unrestricted fitsInduction : (family DataBytesWord32DecodeResult) .
1127          (constructor
1128            DataBytesWord32DecodeResult
1129            DataBytesWord32Decoded
1130            (constructor
1131              ModelWord32
1132              ModelWord32Value
1133              (dataBytesByteAtValidated input zero)
1134              (dataBytesByteAtValidated input dataBytesNaturalOne)
1135              (dataBytesByteAtValidated input dataBytesNaturalTwo)
1136              (dataBytesByteAtValidated input dataBytesNaturalThree))
1137            (dataBytesDropValidated dataBytesNaturalFour input))))
1138      (naturalLessOrEqual dataBytesNaturalFour (bytes-length input))))

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.