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 1184–1206

dataBytesReadWord64BE

Full file
1184def dataBytesReadWord64BE =
1185  (lambda unrestricted input : Bytes .
1186    (nat-eliminate
1187      (lambda unrestricted current : Nat . (family DataBytesWord64DecodeResult))
1188      dataBytesWord64Failure
1189      (lambda unrestricted fitsPredecessor : Nat .
1190        (lambda unrestricted fitsInduction : (family DataBytesWord64DecodeResult) .
1191          (constructor
1192            DataBytesWord64DecodeResult
1193            DataBytesWord64Decoded
1194            (constructor
1195              ModelWord64
1196              ModelWord64Value
1197              (dataBytesByteAtValidated input dataBytesNaturalSeven)
1198              (dataBytesByteAtValidated input dataBytesNaturalSix)
1199              (dataBytesByteAtValidated input dataBytesNaturalFive)
1200              (dataBytesByteAtValidated input dataBytesNaturalFour)
1201              (dataBytesByteAtValidated input dataBytesNaturalThree)
1202              (dataBytesByteAtValidated input dataBytesNaturalTwo)
1203              (dataBytesByteAtValidated input dataBytesNaturalOne)
1204              (dataBytesByteAtValidated input zero))
1205            (dataBytesDropValidated dataBytesNaturalEight input))))
1206      (naturalLessOrEqual dataBytesNaturalEight (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.