Source/Packages

Compiler.Planning.Protocol

packages/compiler/planning/src/Compiler/Planning/Protocol.alpha

487 lines8 declarations22.1 KiBSHA-256 21f495cf84da

def · lines 26–39

protocolCheckThen

Full file
26def protocolCheckThen =
27  (lambda unrestricted first : (family StdResult (family ProtocolFailure) Nat) .
28    (lambda unrestricted next : (family StdResult (family ProtocolFailure) Nat) .
29      (eliminate
30        StdResult
31        (lambda unrestricted current : (family StdResult (family ProtocolFailure) Nat) .
32          (family StdResult (family ProtocolFailure) Nat))
33        first
34        (branch
35          StdFailure
36          error
37          .
38          (constructor StdResult StdFailure (family ProtocolFailure) Nat error))
39        (branch StdSuccess value . next))))

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.