~/jendhub

def no_carry

stelliferous@0.0.2.0 · proofs/u32_shift.bend:37

import stelliferous@0.0.2.0/proofs/u32_shift.bend as U32Shift
import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

37def no_carry(+w: Word(32n),+c: Bool) -> Goal(w,c):
38  %WordEncoding.recover(31n,1n,w) : Goal(_,c)
39  parts(c,WordEncoding.split(31n,1n,w))

Uses (6)

Used by (1)