TraceContext.Parse.nonzero_result: def of bend-trace-context@0.2.0.0
Import: import bend-trace-context@0.2.0.0/trace_context.bend as TraceContext
Lines 409-417 of bend-trace-context@0.2.0.0/trace_context.bend: https://jend.leeeet.dev/read.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&start_line=409&end_line=417

import Base
import bend-trace-context@0.2.0.0/src/digits.bend as Digits

# Attach the proof that digits are not all zero, or fail with ZeroId naming
# the field.
def Parse.nonzero_result(-n: Nat, result: Maybe<&2, Digits.NonZero<n>>, field: Field) ->
  Result<&2, &2, Error, Digits.NonZero<n>>:
  match result:
    case None{}:
      Fail{ZeroId{field}}
    case Some{id}:
      Done{id}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=NonZero
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Field