def cy

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32alg.bend:20

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend as AD

20def cy(+n: Nat, +a: Word(n), +b: Word(n), +c: Bool) -> Nat:
21  S.bit_value(AD.carry_out(n, a, b, c))