def join

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/src/wide.bend:103

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend as NM

103# Exact limb boundary used by the host bridge; limbs themselves are primitive U32.
104def join(n: Nat, +m: Nat, a: Word(n), b: Word(m)) -> Word(Nat.add(n, m)):
105  NM.join(n, m, a, b)