Source/Packages

Runtime.NativePhysicalProgram

packages/execution/src/Runtime/NativePhysicalProgram.alpha

1,008 lines185 declarations40.0 KiBSHA-256 e6bb0cdfb8f4

def · lines 569–578

nativePhysicalRequireBytes

Full file
569def nativePhysicalRequireBytes =
570  (lambda unrestricted payload : Bytes .
571    (lambda unrestricted error : (family NativePhysicalErrorCode) .
572      (nat-eliminate
573        (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
574        (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error)
575        (lambda unrestricted predecessor : Nat .
576          (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
577            (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
578        (bytes-length payload))))

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.