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 1160–1182

dataBytesReadWord64LE

Full file
1160def dataBytesReadWord64LE =
1161  (lambda unrestricted input : Bytes .
1162    (nat-eliminate
1163      (lambda unrestricted current : Nat . (family DataBytesWord64DecodeResult))
1164      dataBytesWord64Failure
1165      (lambda unrestricted fitsPredecessor : Nat .
1166        (lambda unrestricted fitsInduction : (family DataBytesWord64DecodeResult) .
1167          (constructor
1168            DataBytesWord64DecodeResult
1169            DataBytesWord64Decoded
1170            (constructor
1171              ModelWord64
1172              ModelWord64Value
1173              (dataBytesByteAtValidated input zero)
1174              (dataBytesByteAtValidated input dataBytesNaturalOne)
1175              (dataBytesByteAtValidated input dataBytesNaturalTwo)
1176              (dataBytesByteAtValidated input dataBytesNaturalThree)
1177              (dataBytesByteAtValidated input dataBytesNaturalFour)
1178              (dataBytesByteAtValidated input dataBytesNaturalFive)
1179              (dataBytesByteAtValidated input dataBytesNaturalSix)
1180              (dataBytesByteAtValidated input dataBytesNaturalSeven))
1181            (dataBytesDropValidated dataBytesNaturalEight input))))
1182      (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.