Source/Packages

Checkpoint.NativeTreePublication

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

1,138 lines56 declarations55.0 KiBSHA-256 a6e4225ebb3a

def · lines 139–155

nativeTreePreviousShard

Full file
139def nativeTreePreviousShard =
140  (lambda unrestricted paths : (family NativeTreePaths) .
141    (eliminate
142      NativeTreePaths
143      (lambda unrestricted current : (family NativeTreePaths) . (pi unrestricted index : Nat . Nat))
144      paths
145      (branch
146        NativeTreePathsOf
147        group
148        shard
149        candidate
150        committed
151        shardCandidate
152        shardCommitted
153        directory
154        .
155        shard)))

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.