def NonZero.new

bend-trace-context@0.2.0.0 · src/digits.bend:125

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

import Base

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

Uses (6)

Used by (3)