Digits.NonZero.new: def of bend-trace-context@0.2.0.0
Import: import bend-trace-context@0.2.0.0/src/digits.bend as Digits
Lines 125-127 of bend-trace-context@0.2.0.0/src/digits.bend: https://jend.leeeet.dev/read.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&start_line=125&end_line=127

import Base

# Attach the proof that the digits are not all zero, or None when they are.
def NonZero.new(+n: Nat, +digits: Digits(n)) -> Maybe<&2, NonZero<n>>:
  NonZero.new.checked(n, digits, Digits.is_zero(n, digits), {==})

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=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.is_zero
  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/src/digits.bend&name=NonZero.new.checked