Source/Packages

Checkpoint.Envelope

packages/execution/persistence/src/Checkpoint/Envelope.alpha

280 lines55 declarations15.0 KiBSHA-256 3098c6153ea6

def · lines 195–199

checkpointEnvelopeSlice

Full file
---- the model's reading of a checkpoint file ----
195def checkpointEnvelopeSlice =
196  (lambda unrestricted file : Bytes .
197    (lambda unrestricted offset : Nat .
198      (lambda unrestricted length : Nat .
199        (dataBytesTakeValidated length (dataBytesDropValidated offset file)))))

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.