Source/Packages

Std.Foundation

packages/foundation/standard/src/Std/Foundation.alpha

329 lines52 declarations12.3 KiBSHA-256 7818c29d5c7c

def · lines 280–289

stdResultBind

Full file
Compose checked operations without replacing an earlier error with a later default. The continuation receives a value only in the success branch.
280def stdResultBind =
281  (lambda erased errorType : Type 0 .
282    (lambda erased inputType : Type 0 .
283      (lambda erased outputType : Type 0 .
284        (lambda unrestricted input : (family StdResult errorType inputType) .
285          (lambda unrestricted next : (pi unrestricted value : inputType . (family StdResult errorType outputType)) .
286            (eliminate StdResult
287              (lambda unrestricted current : (family StdResult errorType inputType) . (family StdResult errorType outputType)) input
288              (branch StdFailure error . (constructor StdResult StdFailure errorType outputType error))
289              (branch StdSuccess value . (next value))))))))

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.