type NonZero

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

import Base

108# n digits that are not all zero. `evidence` is the proof. The equality is
109# checked statically; compiled evidence is a null placeholder. Keeping its
110# binder usable lets later proofs recover and reuse this guarantee. Even direct
111# construction must supply a proof that these digits are not zero.
112type NonZero<-n: Nat> is Data:
113  NonZero{digits: Digits(n), evidence: {Digits.is_zero(n, digits) == False{} : Bool}}