def mex

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mul.bend:202

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64mul

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_multiplication.bend as WM

202def mex(x: U32, y: U32) -> Nat:
203  match x y:
204    case U32{a} U32{b}:
205      WM.excess(32n, 32n, a, b, Word.zero(32n))

Uses (4)

Used by (6)