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.