AlphaGitHub
Source/Packages

Std.Numeric.Profile

packages/foundation/standard/src/Std/Numeric/Profile.alpha

736 lines139 declarations26.5 KiBSHA-256 2450517e3794
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 501–515

stdProfileAdmitsOn

Full file
the same on a device: a profile of another device is rejected first
501def stdProfileAdmitsOn =
502  (lambda unrestricted device : (family StdNumericProfileIdentity) .
503    (lambda unrestricted profile : (family StdNumericProfile) .
504      (lambda unrestricted format : (family StdNumericFormat) .
505        (lambda unrestricted operation : (family StdNumericOperation) .
506          (stdAdmissionWhen
507            (bytes-equal
508              (stdNumericProfileIdentityBytes device)
509              (stdNumericProfileIdentityBytes (stdNumericProfileIdentityOf profile)))
510            (stdProfileAdmits profile format operation)
511            (constructor
512              StdNumericAdmission
513              StdAdmissionRejected
514              b"ALPHA-ADMISSION-UNSUPPORTED-DEVICE"
515              b"the profile belongs to another device than the one requested"))))))

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.