AlphaGitHub
Source/Systems

Bob.Build.NativeHost

systems/bob/src/Bob/Build/NativeHost.alpha

882 lines46 declarations32.2 KiBSHA-256 3f8d3aa22d4e
Download exact fileView at revision426597bda5753d86c4

def · lines 771–783

bobHostAdmitted

Full file
the host's side (its schedule, and the AdamW sites the realization placed), then (only when it holds) the device's (Bob.Build.PhysicalComponents.bobDeviceHazard)
771def bobHostAdmitted =
772  (lambda unrestricted qmdLength : Nat .
773    (lambda unrestricted pushLength : Nat .
774      (lambda unrestricted gpfifoLength : Nat .
775        (lambda unrestricted realized : (family BobRealizedTables) .
776          (nat-eliminate
777            (lambda unrestricted host : Nat . Nat)
778            0
779            (lambda unrestricted p : Nat .
780              (lambda unrestricted ignored : Nat . (naturalIsZero (bobDeviceHazardOf p))))
781            (naturalAnd
782              (bobHostLearnerAdmitted (bobHostLayout b"" qmdLength pushLength) realized)
783              (bobHostCertified qmdLength pushLength gpfifoLength)))))))

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.