Digits.NonZero.new.checked: def of bend-trace-context@0.2.0.0
Import: import bend-trace-context@0.2.0.0/src/digits.bend as Digits
Lines 115-123 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=115&end_line=123

import Base

# Carry the equation into the branch: matching status refines its right side.
# The value is built only in the False case, where the equation is the proof.
def NonZero.new.checked(-n: Nat, digits: Digits(n), status: Bool,
  evidence: {Digits.is_zero(n, digits) == status : Bool}) -> Maybe<&2, NonZero<n>>:
  match status:
    case True{}:
      None{}
    case False{}:
      Some{NonZero{digits, evidence}}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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