AlphaGitHub
Source/Systems

PartitionedRegression.Build.CoordinateDevice

systems/partitioned-regression/src/PartitionedRegression/Build/CoordinateDevice.alpha

572 lines19 declarations27.0 KiBSHA-256 19b30f5eebcb
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 172–187

cdTrainingAdmitted

Full file
172def cdTrainingAdmitted =
173  (lambda unrestricted worker : Nat .
174    (lambda unrestricted resume : Nat .
175      (lambda unrestricted epoch : Nat .
176        (lambda unrestricted steps : Nat .
177          (naturalAnd
178            (naturalLessOrEqual worker 1)
179            (naturalAnd
180              (naturalLessOrEqual resume 1)
181              (naturalAnd
182                (naturalNonzero epoch)
183                (naturalAnd
184                  (naturalLessOrEqual (naturalAdd epoch resume) regionFrameWordLimit)
185                  (naturalAnd
186                    (naturalNonzero steps)
187                    (naturalLessOrEqual (naturalMultiply cdmIssueCount steps) regionFrameWordLimit))))))))))

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.