def res_val

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/proof.bend:25

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M

25# the value of a successful result, 0 on an error
26def res_val(r: Result<&2, &2, M.MathError, Nat>) -> Nat:
27  match r:
28    case Done{x}:
29      x
30    case Fail{e}:
31      0n