---- ownership and shapes ----
Coordinate i belongs to owner i mod n.
257def dpoOwns =
258 (lambda unrestricted owners : Nat .
259 (lambda unrestricted role : Nat .
260 (lambda unrestricted coordinate : Nat .
261 (naturalEqual (naturalModuloUnchecked coordinate owners) role))))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.