AlphaGitHub
Source/Packages

Runtime.NativeIndependentTree

packages/execution/src/Runtime/NativeIndependentTree.alpha

607 lines29 declarations27.9 KiBSHA-256 1a2ac79dd64d
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 139–157

nitOwnOf

Full file
A role holds one interval of the one logical region: its own state words.
139def nitOwnOf =
140  (lambda unrestricted slots : Nat .
141    (lambda unrestricted system : (family IndependentStateSystem slots) .
142      (lambda unrestricted role : Nat .
143        (constructor
144          StdList
145          StdListCons
146          (family CheckpointRegionPartition)
147          (constructor
148            CheckpointRegionPartition
149            CheckpointRegionPartitionOf
150            0
151            (constructor
152              StdList
153              StdListCons
154              (family LogicalInterval)
155              (niInterval slots system role)
156              (constructor StdList StdListEmpty (family LogicalInterval))))
157          (constructor StdList StdListEmpty (family CheckpointRegionPartition))))))

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.