The read replica is resident only with partitioned parameters.
2495def dpoReplicaResidents =
2496 (lambda unrestricted c : Nat .
2497 (lambda unrestricted u : Nat .
2498 (lambda unrestricted system : (family DataParallelSystem c u) .
2499 (lambda unrestricted p : Nat .
2500 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
2501 (lambda unrestricted rest : (family ArenaResidents) .
2502 (nat-eliminate
2503 (lambda unrestricted current : Nat . (family ArenaResidents))
2504 rest
2505 (lambda unrestricted previous : Nat .
2506 (lambda unrestricted ignored : (family ArenaResidents) .
2507 (constructor
2508 ArenaResidents
2509 ArenaResidentsNext
2510 (constructor
2511 ArenaResident
2512 ArenaResidentValue
2513 b"data-parallel-read-replica"
2514 (dpoReplicaAt c u system layout)
2515 (dpoReplicaBytes c u system p)
2516 dpWord)
2517 rest)))
2518 p)))))))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.