AlphaGitHub
Source/Packages

Runtime.NativeProtocol

packages/execution/src/Runtime/NativeProtocol.alpha

446 lines17 declarations22.3 KiBSHA-256 5f3a02d1b9cf
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 52–61

nativeProtocolDecisionState

Full file
52def nativeProtocolDecisionState =
53  (lambda erased decision : Type 0 .
54    (lambda erased payload : Type 0 .
55      (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) .
56        (eliminate
57          NativeProtocolDecisionBinding
58          (lambda unrestricted current : (family NativeProtocolDecisionBinding decision payload) .
59            (pi unrestricted selector : decision . Nat))
60          binding
61          (branch NativeProtocolDecisionBindingOf source state scratch frame . state)))))

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.