AlphaGitHub
Source/Packages

Runtime.NativePhysicalProgram

packages/execution/src/Runtime/NativePhysicalProgram.alpha

1,746 lines210 declarations66.5 KiBSHA-256 4105493447e0
Download exact fileView at revision426597bda5753d86c4

def · lines 1524–1554

nativePhysicalArgumentsScopeAdmission

Full file
1524def nativePhysicalArgumentsScopeAdmission =
1525  (lambda unrestricted stateBytes : Nat .
1526    (lambda unrestricted slots : Nat .
1527      (lambda unrestricted payloadBytes : Nat .
1528        (lambda unrestricted arguments : (family NativePhysicalArguments) .
1529          (eliminate
1530            NativePhysicalArguments
1531            (lambda unrestricted current : (family NativePhysicalArguments) . Nat)
1532            arguments
1533            (branch
1534              NativePhysicalArgumentsValue
1535              a0
1536              a1
1537              a2
1538              a3
1539              a4
1540              a5
1541              .
1542              (naturalAnd
1543                (nativePhysicalOperandScopeAdmission stateBytes slots payloadBytes a0)
1544                (naturalAnd
1545                  (nativePhysicalOperandScopeAdmission stateBytes slots payloadBytes a1)
1546                  (naturalAnd
1547                    (nativePhysicalOperandScopeAdmission stateBytes slots payloadBytes a2)
1548                    (naturalAnd
1549                      (nativePhysicalOperandScopeAdmission stateBytes slots payloadBytes a3)
1550                      (naturalAnd
1551                        (nativePhysicalOperandScopeAdmission stateBytes slots payloadBytes a4)
1552                        (naturalAnd
1553                          (nativePhysicalOperandScopeAdmission stateBytes slots payloadBytes a5)
1554                          1))))))))))))

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.