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 1140–1158

dataBytesReadWord32BE

Full file
1140def dataBytesReadWord32BE =
1141  (lambda unrestricted input : Bytes .
1142    (nat-eliminate
1143      (lambda unrestricted current : Nat . (family DataBytesWord32DecodeResult))
1144      dataBytesWord32Failure
1145      (lambda unrestricted fitsPredecessor : Nat .
1146        (lambda unrestricted fitsInduction : (family DataBytesWord32DecodeResult) .
1147          (constructor
1148            DataBytesWord32DecodeResult
1149            DataBytesWord32Decoded
1150            (constructor
1151              ModelWord32
1152              ModelWord32Value
1153              (dataBytesByteAtValidated input dataBytesNaturalThree)
1154              (dataBytesByteAtValidated input dataBytesNaturalTwo)
1155              (dataBytesByteAtValidated input dataBytesNaturalOne)
1156              (dataBytesByteAtValidated input zero))
1157            (dataBytesDropValidated dataBytesNaturalFour input))))
1158      (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.