Source/Packages

Checkpoint.NativePeerPublication

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

478 lines34 declarations22.1 KiBSHA-256 2ce6ac127ae2

def · lines 162–172

nativePeerEachOwner

Full file
`body owner` for owners 1..peers, in order.
162def nativePeerEachOwner =
163  (lambda unrestricted peers : Nat .
164    (lambda unrestricted body : (pi unrestricted owner : Nat . (pi unrestricted rest : (family NativePhysicalCommands) . (family NativePhysicalCommands))) .
165      (lambda unrestricted tail : (family NativePhysicalCommands) .
166        (stdListFold
167          Nat
168          (family NativePhysicalCommands)
169          (lambda unrestricted index : Nat .
170            (lambda unrestricted rest : (family NativePhysicalCommands) . (body (succ index) rest)))
171          tail
172          (stdListNaturalsBelow peers)))))

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.