def Parse.nonzero_result

bend-trace-context@0.2.0.0 · trace_context.bend:409

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

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