def NonZero.new.checked

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

import Base

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